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

Theorem com4l 78
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 75 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ( th  ->  ta ) ) ) )
32com34 77 1  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4t  79  com4r  80  com14  82  com5l  86  3impd  1165  merco2  1501  ax12b  1689  onint  4668  tfrlem1  6478  oalimcl  6645  oeordsuc  6679  fisup2g  7307  zorn2lem7  8219  inar1  8487  rpnnen1lem5  10438  expnbnd  11323  facwordi  11395  unbenlem  13052  fiinopn  16753  cmpsublem  17232  dvcnvrelem1  19468  spansncol  22261  atcvat4i  23091  sumdmdlem  23112  nocvxminlem  24902  axcontlem4  25154  axcont  25163  broutsideof2  25304  brfi1uzind  27497  pm2.43cbi  28025  cvrat4  29701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator