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  3imp3i2anOLD  1436  3expd  1445  elpwunsn  4360  onint  7141  tfindsg  7206  findsg  7239  tfrlem9  7633  tz7.49  7692  oaordi  7779  odi  7812  nnaordi  7851  nndi  7856  php  8299  fiint  8392  carduni  9006  dfac2b  9152  dfac2OLD  9154  axcclem  9480  zorn2lem6  9524  zorn2lem7  9525  grur1a  9842  mulcanpi  9923  ltexprlem7  10065  axpre-sup  10191  xrsupsslem  12341  xrinfmsslem  12342  supxrunb1  12353  supxrunb2  12354  mulgnnass  17783  mulgnnassOLD  17784  fiinopn  20925  axcont  26076  sumdmdlem  29611  matunitlindflem1  33731  ee33VD  39631
 Copyright terms: Public domain W3C validator