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

Theorem com15 93
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 92 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ta  ->  (
ph  ->  et ) ) ) ) )
32com4r 86 1  |-  ( ta 
->  ( ps  ->  ( ch  ->  ( th  ->  (
ph  ->  et ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  injresinjlem  11905  brfi1uzind  12513  swrdswrdlem  12664  2cshwcshw  12773  spthonepeq  24412  wlkdvspthlem  24432  erclwwlktr  24638  erclwwlkntr  24650  el2wlkonot  24692  3cyclfrgrarn1  24835  frgranbnb  24843  vdn0frgrav2  24847  frgrancvvdeqlemB  24862  usg2spot2nb  24889  numclwwlkovf2ex  24910  frgrareg  24941  frgraregord013  24942  zerdivemp1  25259  zerdivemp1x  30285  usgra2pthlem1  32143
  Copyright terms: Public domain W3C validator