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

Theorem com45 85
Description: Commutation of antecedents. Swap 4th and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
Hypothesis
Ref Expression
com5.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
Assertion
Ref Expression
com45  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  ( th  ->  et )
) ) ) )

Proof of Theorem com45
StepHypRef Expression
1 com5.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
2 pm2.04 78 . 2  |-  ( ( th  ->  ( ta  ->  et ) )  -> 
( ta  ->  ( th  ->  et ) ) )
31, 2syl8 67 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  ( th  ->  et )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com35  86  com25  87  com5l  88  islmhm2  16077  dfon2lem8  25368  ad5ant13  28269  ad5ant14  28270  ad5ant15  28271  ad5ant23  28272  ad5ant24  28273  ad5ant25  28274  ad5ant245  28275  ad5ant235  28277  ad5ant123  28278  ad5ant124  28279  ad5ant134  28281  ad5ant135  28282  ad5ant145  28283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator