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  4584  onint  4602  tfindsg  4667  findsg  4699  tfrlem9  6417  tz7.49  6473  oaordi  6560  odi  6593  nnaordi  6632  nndi  6637  php  7061  fiint  7149  carduni  7630  dfac2  7773  axcclem  8099  zorn2lem6  8144  zorn2lem7  8145  grur1a  8457  mulcanpi  8540  ltexprlem7  8682  axpre-sup  8807  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  spwmo  14351  mulgnnass  14611  fiinopn  16663  sumdmdlem  23014  axcont  24676  eqfnung2  25221  glmrngo  25585  bwt2  25695  cmpmon  25918  ee33VD  28971
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator