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

Theorem com45 86
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 79 . 2  |-  ( ( th  ->  ( ta  ->  et ) )  -> 
( ta  ->  ( th  ->  et ) ) )
31, 2syl8 68 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  ( th  ->  et )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com35  87  com25  88  com5l  89  islmhm2  16145  dfon2lem8  25448  ad5ant13  28645  ad5ant14  28646  ad5ant15  28647  ad5ant23  28648  ad5ant24  28649  ad5ant25  28650  ad5ant245  28651  ad5ant235  28653  ad5ant123  28654  ad5ant124  28655  ad5ant134  28657  ad5ant135  28658  ad5ant145  28659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator