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  1214  elpwunsn  4055  onint  6615  tfindsg  6680  findsg  6712  tfrlem9  7056  tz7.49  7112  oaordi  7197  odi  7230  nnaordi  7269  nndi  7274  php  7703  fiint  7799  carduni  8365  dfac2  8514  axcclem  8840  zorn2lem6  8884  zorn2lem7  8885  grur1a  9200  mulcanpi  9281  ltexprlem7  9423  axpre-sup  9549  xrsupsslem  11509  xrinfmsslem  11510  supxrunb1  11522  supxrunb2  11523  mulgnnass  16149  fiinopn  19388  bwthOLD  19889  axcont  24257  sumdmdlem  27315  eel32131  33377  ee33VD  33547
  Copyright terms: Public domain W3C validator