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

Theorem com3r 84
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 83 . 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  85  com3l  86  com14  93  expd  450  ad5ant23  1295  ad5ant24  1296  ad5ant25  1297  mob  3354  otiunsndisj  4896  issref  5415  sotri2  5431  sotri3  5432  relresfld  5565  limuni3  6922  poxp  7154  soxp  7155  tz7.49  7405  omwordri  7517  odi  7524  omass  7525  oewordri  7537  nndi  7568  nnmass  7569  r1sdom  8498  tz9.12lem3  8513  cardlim  8659  carduni  8668  alephordi  8758  alephval3  8794  domtriomlem  9125  axdc3lem2  9134  axdc3lem4  9136  axcclem  9140  zorn2lem5  9183  zorn2lem6  9184  axdclem2  9203  alephval2  9251  gruen  9491  grur1a  9498  grothomex  9508  nqereu  9608  distrlem5pr  9706  psslinpr  9710  ltaprlem  9723  suplem1pr  9731  lbreu  10825  fleqceilz  12473  caubnd  13895  divconjdvds  14824  algcvga  15079  algfx  15080  gsummatr01lem3  20230  fiinopn  20479  hausnei  20890  hausnei2  20915  cmpsublem  20960  cmpsub  20961  fcfneii  21599  ppiublem1  24672  nb3graprlem1  25774  cusgrasize2inds  25799  wlkdvspthlem  25931  usgra2wlkspth  25943  clwwlkprop  26092  clwwlkgt0  26093  clwlkisclwwlklem1  26109  clwwlkf  26116  vdgn1frgrav2  26347  frgrancvvdeqlemB  26359  frgrancvvdeqlemC  26360  frgraregord013  26439  chintcli  27408  h1datomi  27658  strlem3a  28329  hstrlem3a  28337  mdexchi  28412  cvbr4i  28444  mdsymlem4  28483  mdsymlem6  28485  3jaodd  30684  frr3g  30857  ifscgr  31155  bj-mo3OLD  31856  wepwsolem  36454  rp-fakeimass  36700  ee233  37570  iccpartgt  39790  lighneal  39891  nb3grprlem1  40630  cusgrsize2inds  40691  1wlk1walk  40865  clwlkclwwlklem2  41231  clwwlksf  41244  vdgn1frgrv2  41488  frgrncvvdeqlemB  41499  frgrncvvdeqlemC  41500  av-frgrareggt1  41569  av-frgraregord013  41571  ldepspr  42078
  Copyright terms: Public domain W3C validator