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

Theorem com4l 80
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 77 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 79 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4t  81  com4r  82  com14  84  com5l  88  3impd  1167  merco2  1507  onint  4738  tfrlem1  6599  oalimcl  6766  oeordsuc  6800  fisup2g  7431  zorn2lem7  8342  inar1  8610  rpnnen1lem5  10564  expnbnd  11467  facwordi  11539  brfi1uzind  11674  unbenlem  13235  fiinopn  16933  cmpsublem  17420  dvcnvrelem1  19858  spansncol  23027  atcvat4i  23857  sumdmdlem  23878  nocvxminlem  25562  axcontlem4  25814  axcont  25823  broutsideof2  25964  pm2.43cbi  28316  cvrat4  29929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator