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

Theorem com4l 81
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by 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 78 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 80 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4t  82  com4r  83  com14  85  com5l  89  3impd  1168  merco2  1511  onint  4804  tfrlem1  6665  oalimcl  6832  oeordsuc  6866  fisup2g  7500  zorn2lem7  8413  inar1  8681  rpnnen1lem5  10635  expnbnd  11539  facwordi  11611  brfi1uzind  11746  unbenlem  13307  fiinopn  17005  cmpsublem  17493  bwth  17504  dvcnvrelem1  19932  spansncol  23101  atcvat4i  23931  sumdmdlem  23952  nocvxminlem  25676  axcontlem4  25937  axcont  25946  broutsideof2  26087  pm2.43cbi  28699  cvrat4  30338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator