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

Theorem com4t 79
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 78 . 2  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ph  ->  ta ) ) ) )
32com4l 78 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com4r  80  com24  81  mopick  2218  tfindsg  4667  isofrlem  5853  tfr3  6431  pssnn  7097  dfac5  7771  cfcoflem  7914  isf32lem12  8006  ltexprlem7  8682  dirtr  14374  chirredlem1  22986  mdsymlem4  23002  cdj3lem2b  23033  eqfnung2  25221  injsurinj  25252  prl  25270  3cyclfrgrarn1  28435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator