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  451  ad5ant23OLD  1339  ad5ant24OLD  1341  ad5ant25OLD  1343  mob  3421  otiunsndisj  5009  issref  5544  sotri2  5560  sotri3  5561  relresfld  5700  limuni3  7094  poxp  7334  soxp  7335  tz7.49  7585  omwordri  7697  odi  7704  omass  7705  oewordri  7717  nndi  7748  nnmass  7749  r1sdom  8675  tz9.12lem3  8690  cardlim  8836  carduni  8845  alephordi  8935  alephval3  8971  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axcclem  9317  zorn2lem5  9360  zorn2lem6  9361  axdclem2  9380  alephval2  9432  gruen  9672  grur1a  9679  grothomex  9689  nqereu  9789  distrlem5pr  9887  psslinpr  9891  ltaprlem  9904  suplem1pr  9912  lbreu  11011  fleqceilz  12693  caubnd  14142  divconjdvds  15084  algcvga  15339  algfx  15340  gsummatr01lem3  20511  fiinopn  20754  hausnei  21180  hausnei2  21205  cmpsublem  21250  cmpsub  21251  fcfneii  21888  ppiublem1  24972  nb3grprlem1  26326  cusgrsize2inds  26405  wlk1walk  26591  clwlkclwwlklem2  26966  clwwlkf  27010  vdgn1frgrv2  27276  frgrncvvdeqlem8  27286  frgrncvvdeqlem9  27287  frgrreggt1  27380  frgrregord013  27382  chintcli  28318  h1datomi  28568  strlem3a  29239  hstrlem3a  29247  mdexchi  29322  cvbr4i  29354  mdsymlem4  29393  mdsymlem6  29395  3jaodd  31721  frr3g  31904  ifscgr  32276  bj-mo3OLD  32957  wepwsolem  37929  rp-fakeimass  38174  ee233  39042  iccpartgt  41688  lighneal  41853  ldepspr  42587
  Copyright terms: Public domain W3C validator