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  1213  elpwunsn  4074  onint  6625  tfindsg  6690  findsg  6722  tfrlem9  7066  tz7.49  7122  oaordi  7207  odi  7240  nnaordi  7279  nndi  7284  php  7713  fiint  7809  carduni  8374  dfac2  8523  axcclem  8849  zorn2lem6  8893  zorn2lem7  8894  grur1a  9209  mulcanpi  9290  ltexprlem7  9432  axpre-sup  9558  xrsupsslem  11510  xrinfmsslem  11511  supxrunb1  11523  supxrunb2  11524  mulgnnass  16042  fiinopn  19279  bwthOLD  19779  axcont  24093  sumdmdlem  27151  eel32131  32945  ee33VD  33115
  Copyright terms: Public domain W3C validator