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  3imp3i2an  1275  3expd  1281  elpwunsn  4195  onint  6942  tfindsg  7007  findsg  7040  tfrlem9  7426  tz7.49  7485  oaordi  7571  odi  7604  nnaordi  7643  nndi  7648  php  8088  fiint  8181  carduni  8751  dfac2  8897  axcclem  9223  zorn2lem6  9267  zorn2lem7  9268  grur1a  9585  mulcanpi  9666  ltexprlem7  9808  axpre-sup  9934  xrsupsslem  12080  xrinfmsslem  12081  supxrunb1  12092  supxrunb2  12093  mulgnnass  17497  mulgnnassOLD  17498  fiinopn  20631  axcont  25756  sumdmdlem  29126  matunitlindflem1  33037  ee33VD  38598
  Copyright terms: Public domain W3C validator