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  2205  tfindsg  4651  isofrlem  5837  tfr3  6415  pssnn  7081  dfac5  7755  cfcoflem  7898  isf32lem12  7990  ltexprlem7  8666  dirtr  14358  chirredlem1  22970  mdsymlem4  22986  cdj3lem2b  23017  eqfnung2  25118  injsurinj  25149  prl  25167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator