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

Theorem com45 83
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 76 . 2  |-  ( ( th  ->  ( ta  ->  et ) )  -> 
( ta  ->  ( th  ->  et ) ) )
31, 2syl8 65 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  ( th  ->  et )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com35  84  com25  85  com5l  86  islmhm2  15811  dfon2lem8  24217  ad5ant12  28527  ad5ant13  28528  ad5ant14  28529  ad5ant15  28530  ad5ant23  28531  ad5ant24  28532  ad5ant25  28533  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  ad5ant123  28537  ad5ant124  28538  ad5ant125  28539  ad5ant134  28540  ad5ant135  28541  ad5ant145  28542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator