MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com4l Structured version   Unicode version

Theorem com4l 84
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.)
Hypothesis
Ref Expression
com4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com4l  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )

Proof of Theorem com4l
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com3l 81 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 83 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com4t  85  com4r  86  com14  88  com5l  92  3impd  1202  merco2  1544  onint  6511  oalimcl  7104  oeordsuc  7138  fisup2g  7822  zorn2lem7  8777  inar1  9048  rpnnen1lem5  11089  expnbnd  12105  facwordi  12177  brfi1uzind  12332  unbenlem  14082  fiinopn  18641  cmpsublem  19129  bwthOLD  19141  dvcnvrelem1  21617  axcontlem4  23360  axcont  23369  spansncol  25118  atcvat4i  25948  sumdmdlem  25969  nocvxminlem  27970  broutsideof2  28292  pm2.43cbi  31536  cvrat4  33406
  Copyright terms: Public domain W3C validator