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

Theorem com15 89
Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
Hypothesis
Ref Expression
com5.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
Assertion
Ref Expression
com15  |-  ( ta 
->  ( ps  ->  ( ch  ->  ( th  ->  (
ph  ->  et ) ) ) ) )

Proof of Theorem com15
StepHypRef Expression
1 com5.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
21com5l 88 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ta  ->  (
ph  ->  et ) ) ) ) )
32com4r 82 1  |-  ( ta 
->  ( ps  ->  ( ch  ->  ( th  ->  (
ph  ->  et ) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  injresinjlem  11199  brfi1uzind  11715  spthonepeq  21587  wlkdvspthlem  21607  zerdivemp1  22022  zerdivemp1x  26571  swrdswrdlem  28198  usgra2pthlem1  28310  el2wlkonot  28336  3cyclfrgrarn1  28402  frgranbnb  28410  vdn0frgrav2  28414  frgrancvvdeqlemB  28427  usg2spot2nb  28454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator