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

Theorem com4r 89
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 88 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com4l 87 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  96  3imp3i2an  1228  3expd  1234  elpwunsn  4023  onint  6648  tfindsg  6713  findsg  6746  tfrlem9  7128  tz7.49  7187  oaordi  7272  odi  7305  nnaordi  7344  nndi  7349  php  7781  fiint  7873  carduni  8440  dfac2  8586  axcclem  8912  zorn2lem6  8956  zorn2lem7  8957  grur1a  9269  mulcanpi  9350  ltexprlem7  9492  axpre-sup  9618  xrsupsslem  11620  xrinfmsslem  11621  supxrunb1  11633  supxrunb2  11634  mulgnnass  16834  fiinopn  19979  axcont  25054  sumdmdlem  28119  ee33VD  37315
  Copyright terms: Public domain W3C validator