MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com3r Structured version   Visualization version   GIF version

Theorem com3r 87
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com3r (𝜒 → (𝜑 → (𝜓𝜃)))

Proof of Theorem com3r
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
32com12 32 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:  com13  88  com3l  89  com14  96  expd  416  mob  3705  otiunsndisj  5401  sotri2  5982  sotri3  5983  relresfld  6120  limuni3  7556  poxp  7811  soxp  7812  tz7.49  8070  omwordri  8187  odi  8194  omass  8195  oewordri  8207  nndi  8238  nnmass  8239  r1sdom  9191  tz9.12lem3  9206  cardlim  9389  carduni  9398  alephordi  9488  alephval3  9524  domtriomlem  9852  axdc3lem2  9861  axdc3lem4  9863  axcclem  9867  zorn2lem5  9910  zorn2lem6  9911  axdclem2  9930  alephval2  9982  gruen  10222  grur1a  10229  grothomex  10239  nqereu  10339  distrlem5pr  10437  psslinpr  10441  ltaprlem  10454  suplem1pr  10462  lbreu  11579  fleqceilz  13210  caubnd  14706  divconjdvds  15653  algcvga  15911  algfx  15912  gsummatr01lem3  21194  fiinopn  21437  hausnei  21864  hausnei2  21889  cmpsublem  21935  cmpsub  21936  fcfneii  22573  ppiublem1  25705  nb3grprlem1  27089  cusgrsize2inds  27162  wlk1walk  27347  clwlkclwwlklem2  27705  clwwlkf  27753  clwwlknonwwlknonb  27812  vdgn1frgrv2  28002  frgrncvvdeqlem8  28012  frgrncvvdeqlem9  28013  frgrreggt1  28099  frgrregord013  28101  chintcli  29035  h1datomi  29285  strlem3a  29956  hstrlem3a  29964  mdexchi  30039  cvbr4i  30071  mdsymlem4  30110  mdsymlem6  30112  3jaodd  32841  frr3g  33018  ifscgr  33402  bj-fvimacnv0  34456  exrecfnlem  34542  wepwsolem  39520  rp-fakeimass  39756  ee233  40730  iccpartgt  43464  lighneal  43653  ldepspr  44456
  Copyright terms: Public domain W3C validator