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  4641  onint  7735  tfindsg  7803  findsg  7839  tfrlem9  8316  tz7.49  8376  oaordi  8473  odi  8506  nnaordi  8546  nndi  8551  php  9131  fiint  9227  carduni  9893  dfac2b  10041  axcclem  10367  zorn2lem6  10411  zorn2lem7  10412  grur1a  10730  mulcanpi  10811  ltexprlem7  10953  axpre-sup  11080  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  mulgnnass  19039  fiinopn  22845  axcont  29049  sumdmdlem  32493  matunitlindflem1  37813  ee33VD  45115
  Copyright terms: Public domain W3C validator