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

Theorem com4r 80
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 79 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com4l 78 1  |-  ( th 
->  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com15  87  3expd  1168  elpwunsn  4568  onint  4586  tfindsg  4651  findsg  4683  tfrlem9  6401  tz7.49  6457  oaordi  6544  odi  6577  nnaordi  6616  nndi  6621  php  7045  fiint  7133  carduni  7614  dfac2  7757  axcclem  8083  zorn2lem6  8128  zorn2lem7  8129  grur1a  8441  mulcanpi  8524  ltexprlem7  8666  axpre-sup  8791  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  spwmo  14335  mulgnnass  14595  fiinopn  16647  sumdmdlem  22998  axcont  24604  eqfnung2  25118  glmrngo  25482  bwt2  25592  cmpmon  25815  ee33VD  28655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator