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

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

Proof of Theorem com4r
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com4t 85 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com4l 84 1  |-  ( th 
->  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com15  93  3expd  1205  elpwunsn  4018  onint  6509  tfindsg  6574  findsg  6606  tfrlem9  6947  tz7.49  7003  oaordi  7088  odi  7121  nnaordi  7160  nndi  7165  php  7598  fiint  7692  carduni  8255  dfac2  8404  axcclem  8730  zorn2lem6  8774  zorn2lem7  8775  grur1a  9090  mulcanpi  9173  ltexprlem7  9315  axpre-sup  9440  xrsupsslem  11373  xrinfmsslem  11374  supxrunb1  11386  supxrunb2  11387  mulgnnass  15766  fiinopn  18639  bwthOLD  19139  axcont  23367  sumdmdlem  25967  eel32131  31748  ee33VD  31918
  Copyright terms: Public domain W3C validator