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

Theorem com3r 85
 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 84 . 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  86  com3l  87  com14  94  expd  451  ad5ant23  1296  ad5ant24  1297  ad5ant25  1298  mob  3355  otiunsndisj  4905  issref  5428  sotri2  5444  sotri3  5445  relresfld  5579  limuni3  6944  poxp  7176  soxp  7177  tz7.49  7427  omwordri  7539  odi  7546  omass  7547  oewordri  7559  nndi  7590  nnmass  7591  r1sdom  8520  tz9.12lem3  8535  cardlim  8681  carduni  8690  alephordi  8780  alephval3  8816  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axcclem  9162  zorn2lem5  9205  zorn2lem6  9206  axdclem2  9225  alephval2  9273  gruen  9513  grur1a  9520  grothomex  9530  nqereu  9630  distrlem5pr  9728  psslinpr  9732  ltaprlem  9745  suplem1pr  9753  lbreu  10852  fleqceilz  12515  caubnd  13946  divconjdvds  14875  algcvga  15130  algfx  15131  gsummatr01lem3  20282  fiinopn  20531  hausnei  20942  hausnei2  20967  cmpsublem  21012  cmpsub  21013  fcfneii  21651  ppiublem1  24727  nb3graprlem1  25980  cusgrasize2inds  26005  wlkdvspthlem  26137  usgra2wlkspth  26149  clwwlkprop  26298  clwwlkgt0  26299  clwlkisclwwlklem1  26315  clwwlkf  26322  vdgn1frgrav2  26553  frgrancvvdeqlemB  26565  frgrancvvdeqlemC  26566  frgraregord013  26645  chintcli  27574  h1datomi  27824  strlem3a  28495  hstrlem3a  28503  mdexchi  28578  cvbr4i  28610  mdsymlem4  28649  mdsymlem6  28651  3jaodd  30850  frr3g  31023  ifscgr  31321  bj-mo3OLD  32022  wepwsolem  36630  rp-fakeimass  36876  ee233  37746  iccpartgt  39965  lighneal  40066  nb3grprlem1  40608  cusgrsize2inds  40669  1wlk1walk  40843  clwlkclwwlklem2  41209  clwwlksf  41222  vdgn1frgrv2  41466  frgrncvvdeqlemB  41477  frgrncvvdeqlemC  41478  av-frgrareggt1  41547  av-frgraregord013  41549  ldepspr  42056
 Copyright terms: Public domain W3C validator