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  3imp3i2an  1277  3expd  1283  elpwunsn  4222  onint  6992  tfindsg  7057  findsg  7090  tfrlem9  7478  tz7.49  7537  oaordi  7623  odi  7656  nnaordi  7695  nndi  7700  php  8141  fiint  8234  carduni  8804  dfac2  8950  axcclem  9276  zorn2lem6  9320  zorn2lem7  9321  grur1a  9638  mulcanpi  9719  ltexprlem7  9861  axpre-sup  9987  xrsupsslem  12134  xrinfmsslem  12135  supxrunb1  12146  supxrunb2  12147  mulgnnass  17570  mulgnnassOLD  17571  fiinopn  20700  axcont  25850  sumdmdlem  29261  matunitlindflem1  33385  ee33VD  38941
  Copyright terms: Public domain W3C validator