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  1415  elpwunsn  4452  onint  7275  tfindsg  7340  findsg  7373  tfrlem9  7766  tz7.49  7825  oaordi  7912  odi  7945  nnaordi  7984  nndi  7989  php  8434  fiint  8527  carduni  9142  dfac2b  9288  dfac2OLD  9290  axcclem  9616  zorn2lem6  9660  zorn2lem7  9661  grur1a  9978  mulcanpi  10059  ltexprlem7  10201  axpre-sup  10328  xrsupsslem  12453  xrinfmsslem  12454  supxrunb1  12465  supxrunb2  12466  mulgnnass  17965  fiinopn  21117  axcont  26329  sumdmdlem  29853  matunitlindflem1  34036  ee33VD  40058
  Copyright terms: Public domain W3C validator