MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com4t Structured version   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  2342  tfindsg  4832  isofrlem  6052  tfr3  6652  pssnn  7319  dfac5  8001  cfcoflem  8144  isf32lem12  8236  ltexprlem7  8911  dirtr  14673  chirredlem1  23885  mdsymlem4  23901  cdj3lem2b  23932  ssfz12  28088  el2wlkonot  28289  3cyclfrgrarn1  28339
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator