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  1352  mo4  2564  elpwunsn  4689  onint  7810  tfindsg  7882  findsg  7920  tfrlem9  8424  tz7.49  8484  oaordi  8583  odi  8616  nnaordi  8655  nndi  8660  php  9245  phpOLD  9257  fiint  9364  fiintOLD  9365  carduni  10019  dfac2b  10169  axcclem  10495  zorn2lem6  10539  zorn2lem7  10540  grur1a  10857  mulcanpi  10938  ltexprlem7  11080  axpre-sup  11207  xrsupsslem  13346  xrinfmsslem  13347  supxrunb1  13358  supxrunb2  13359  mulgnnass  19140  fiinopn  22923  axcont  29006  sumdmdlem  32447  matunitlindflem1  37603  ee33VD  44877
  Copyright terms: Public domain W3C validator