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  1350  mo4  2628  elpwunsn  4584  onint  7494  tfindsg  7559  findsg  7594  tfrlem9  8008  tz7.49  8068  oaordi  8159  odi  8192  nnaordi  8231  nndi  8236  php  8689  fiint  8783  carduni  9398  dfac2b  9545  axcclem  9872  zorn2lem6  9916  zorn2lem7  9917  grur1a  10234  mulcanpi  10315  ltexprlem7  10457  axpre-sup  10584  xrsupsslem  12692  xrinfmsslem  12693  supxrunb1  12704  supxrunb2  12705  mulgnnass  18258  fiinopn  21510  axcont  26774  sumdmdlem  30205  matunitlindflem1  35052  ee33VD  41582
  Copyright terms: Public domain W3C validator