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  2566  elpwunsn  4684  onint  7810  tfindsg  7882  findsg  7919  tfrlem9  8425  tz7.49  8485  oaordi  8584  odi  8617  nnaordi  8656  nndi  8661  php  9247  phpOLD  9259  fiint  9366  fiintOLD  9367  carduni  10021  dfac2b  10171  axcclem  10497  zorn2lem6  10541  zorn2lem7  10542  grur1a  10859  mulcanpi  10940  ltexprlem7  11082  axpre-sup  11209  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  mulgnnass  19127  fiinopn  22907  axcont  28991  sumdmdlem  32437  matunitlindflem1  37623  ee33VD  44899
  Copyright terms: Public domain W3C validator