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  2554  elpwunsn  4689  onint  7794  tfindsg  7866  findsg  7905  tfrlem9  8406  tz7.49  8466  oaordi  8567  odi  8600  nnaordi  8639  nndi  8644  php  9235  phpOLD  9247  fiint  9350  carduni  10006  dfac2b  10155  axcclem  10482  zorn2lem6  10526  zorn2lem7  10527  grur1a  10844  mulcanpi  10925  ltexprlem7  11067  axpre-sup  11194  xrsupsslem  13321  xrinfmsslem  13322  supxrunb1  13333  supxrunb2  13334  mulgnnass  19072  fiinopn  22847  axcont  28859  sumdmdlem  32300  matunitlindflem1  37220  ee33VD  44460
  Copyright terms: Public domain W3C validator