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

Theorem com4r 94
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com4r (𝜃 → (𝜑 → (𝜓 → (𝜒𝜏))))

Proof of Theorem com4r
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4t 93 . 2 (𝜒 → (𝜃 → (𝜑 → (𝜓𝜏))))
32com4l 92 1 (𝜃 → (𝜑 → (𝜓 → (𝜒𝜏))))
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  101  3expd  1354  mo4  2561  elpwunsn  4645  onint  7726  tfindsg  7798  findsg  7837  tfrlem9  8332  tz7.49  8392  oaordi  8494  odi  8527  nnaordi  8566  nndi  8571  php  9157  phpOLD  9169  fiint  9271  carduni  9922  dfac2b  10071  axcclem  10398  zorn2lem6  10442  zorn2lem7  10443  grur1a  10760  mulcanpi  10841  ltexprlem7  10983  axpre-sup  11110  xrsupsslem  13232  xrinfmsslem  13233  supxrunb1  13244  supxrunb2  13245  mulgnnass  18916  fiinopn  22266  axcont  27967  sumdmdlem  31402  matunitlindflem1  36120  ee33VD  43249
  Copyright terms: Public domain W3C validator