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

Theorem com4r 82
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 81 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com4l 80 1  |-  ( th 
->  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com15  89  3expd  1170  elpwunsn  4757  onint  4775  tfindsg  4840  findsg  4872  tfrlem9  6646  tz7.49  6702  oaordi  6789  odi  6822  nnaordi  6861  nndi  6866  php  7291  fiint  7383  carduni  7868  dfac2  8011  axcclem  8337  zorn2lem6  8381  zorn2lem7  8382  grur1a  8694  mulcanpi  8777  ltexprlem7  8919  axpre-sup  9044  xrsupsslem  10885  xrinfmsslem  10886  supxrunb1  10898  supxrunb2  10899  spwmo  14658  mulgnnass  14918  fiinopn  16974  bwth  17473  sumdmdlem  23921  axcont  25915  eel32131  28824  ee33VD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator