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  417  elabgt  3623  mob  3674  otiunsndisj  5476  sotri2  6082  sotri3  6083  relresfld  6227  limuni3  7781  poxp  8053  soxp  8054  tz7.49  8384  omwordri  8512  odi  8519  omass  8520  oewordri  8532  nndi  8563  nnmass  8564  frr3g  9651  r1sdom  9669  tz9.12lem3  9684  cardlim  9867  carduni  9876  alephordi  9969  alephval3  10005  domtriomlem  10337  axdc3lem2  10346  axdc3lem4  10348  axcclem  10352  zorn2lem5  10395  zorn2lem6  10396  axdclem2  10415  alephval2  10467  gruen  10707  grur1a  10714  grothomex  10724  nqereu  10824  distrlem5pr  10922  psslinpr  10926  ltaprlem  10939  suplem1pr  10947  lbreu  12064  fleqceilz  13714  caubnd  15203  divconjdvds  16157  algcvga  16415  algfx  16416  gsummatr01lem3  21958  fiinopn  22202  hausnei  22631  hausnei2  22656  cmpsublem  22702  cmpsub  22703  fcfneii  23340  ppiublem1  26502  ssltun2  27100  nb3grprlem1  28157  cusgrsize2inds  28230  wlk1walk  28416  clwlkclwwlklem2  28773  clwwlkf  28820  clwwlknonwwlknonb  28879  vdgn1frgrv2  29069  frgrncvvdeqlem8  29079  frgrncvvdeqlem9  29080  frgrreggt1  29166  frgrregord013  29168  chintcli  30102  h1datomi  30352  strlem3a  31023  hstrlem3a  31031  mdexchi  31106  cvbr4i  31138  mdsymlem4  31177  mdsymlem6  31179  3jaodd  34092  ifscgr  34561  bj-fvimacnv0  35689  exrecfnlem  35782  wepwsolem  41272  rp-fakeimass  41689  ee233  42706  iccpartgt  45514  lighneal  45698  ldepspr  46449
  Copyright terms: Public domain W3C validator