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

Theorem com4t 81
Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
com4t  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )

Proof of Theorem com4t
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com4l 80 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
32com4l 80 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4r  82  com24  83  mopick  2300  tfindsg  4780  isofrlem  5999  tfr3  6596  pssnn  7263  dfac5  7942  cfcoflem  8085  isf32lem12  8177  ltexprlem7  8852  dirtr  14608  chirredlem1  23741  mdsymlem4  23757  cdj3lem2b  23788  3cyclfrgrarn1  27765
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator