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

Theorem com25 88
Description: Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)
Hypothesis
Ref Expression
com5.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
Assertion
Ref Expression
com25  |-  ( ph  ->  ( ta  ->  ( ch  ->  ( th  ->  ( ps  ->  et )
) ) ) )

Proof of Theorem com25
StepHypRef Expression
1 com5.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ( ta  ->  et )
) ) ) )
21com24 84 . . 3  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ps  ->  ( ta  ->  et )
) ) ) )
32com45 86 . 2  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ta  ->  ( ps  ->  et )
) ) ) )
43com24 84 1  |-  ( ph  ->  ( ta  ->  ( ch  ->  ( th  ->  ( ps  ->  et )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  injresinjlem  11201  brfi1uzind  11717  neindisj2  17189  2ndcdisj  17521  usgrafisinds  21429  cusgrasize2inds  21488  zerdivemp1  22024  zerdivemp1x  26573  swrd0swrd  28199  swrdswrdlem  28200  usgra2wlkspthlem1  28308  frgranbnb  28412  vdn0frgrav2  28416  vdn1frgrav2  28418  frgrawopreg  28440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator