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  419  mob  3656  otiunsndisj  5375  sotri2  5956  sotri3  5957  relresfld  6095  limuni3  7547  poxp  7805  soxp  7806  tz7.49  8064  omwordri  8181  odi  8188  omass  8189  oewordri  8201  nndi  8232  nnmass  8233  r1sdom  9187  tz9.12lem3  9202  cardlim  9385  carduni  9394  alephordi  9485  alephval3  9521  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axcclem  9868  zorn2lem5  9911  zorn2lem6  9912  axdclem2  9931  alephval2  9983  gruen  10223  grur1a  10230  grothomex  10240  nqereu  10340  distrlem5pr  10438  psslinpr  10442  ltaprlem  10455  suplem1pr  10463  lbreu  11578  fleqceilz  13217  caubnd  14710  divconjdvds  15657  algcvga  15913  algfx  15914  gsummatr01lem3  21262  fiinopn  21506  hausnei  21933  hausnei2  21958  cmpsublem  22004  cmpsub  22005  fcfneii  22642  ppiublem1  25786  nb3grprlem1  27170  cusgrsize2inds  27243  wlk1walk  27428  clwlkclwwlklem2  27785  clwwlkf  27832  clwwlknonwwlknonb  27891  vdgn1frgrv2  28081  frgrncvvdeqlem8  28091  frgrncvvdeqlem9  28092  frgrreggt1  28178  frgrregord013  28180  chintcli  29114  h1datomi  29364  strlem3a  30035  hstrlem3a  30043  mdexchi  30118  cvbr4i  30150  mdsymlem4  30189  mdsymlem6  30191  3jaodd  33057  frr3g  33234  ifscgr  33618  bj-fvimacnv0  34701  exrecfnlem  34796  wepwsolem  39984  rp-fakeimass  40218  ee233  41223  iccpartgt  43942  lighneal  44127  ldepspr  44880
 Copyright terms: Public domain W3C validator