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  11650  brfi1uzind  12231  swrdswrdlem  12365  spthonepeq  23498  wlkdvspthlem  23518  zerdivemp1  23933  zerdivemp1x  28773  usgra2pthlem1  30312  el2wlkonot  30400  erclwwlktr  30497  cshwlemma1  30501  erclwwlkntr  30513  3cyclfrgrarn1  30616  frgranbnb  30624  vdn0frgrav2  30628  frgrancvvdeqlemB  30643  usg2spot2nb  30670  numclwwlkovf2ex  30691  frgrareg  30722  frgraregord013  30723
  Copyright terms: Public domain W3C validator