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

Theorem sylcom 30
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)
Hypotheses
Ref Expression
sylcom.1 (𝜑 → (𝜓𝜒))
sylcom.2 (𝜓 → (𝜒𝜃))
Assertion
Ref Expression
sylcom (𝜑 → (𝜓𝜃))

Proof of Theorem sylcom
StepHypRef Expression
1 sylcom.1 . 2 (𝜑 → (𝜓𝜒))
2 sylcom.2 . . 3 (𝜓 → (𝜒𝜃))
32a2i 14 . 2 ((𝜓𝜒) → (𝜓𝜃))
41, 3syl 17 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:  syl5com  31  syl6  35  syli  39  pm2.18d  127  mpbidi  241  2eu6  2657  r19.12OLD  3315  dmcosseq  5987  dmcosseqOLD  5988  iss  6053  funopg  6600  limuni3  7873  frxp  8151  wfrlem12OLD  8360  tz7.49  8485  dif1ennnALT  9311  enp1iOLD  9314  frfi  9321  unblem3  9330  isfinite2  9334  iunfi  9383  tcrank  9924  infdif  10248  isf34lem6  10420  axdc3lem4  10493  suplem1pr  11092  uzwo  12953  gsumcom2  19993  cmpsublem  23407  nrmhaus  23834  metrest  24537  finiunmbl  25579  h1datomi  31600  chirredlem1  32409  fnrelpredd  35103  mclsax  35574  lineext  36077  in-ax8  36225  ss-ax8  36226  onsucconni  36438  cbveud  37373  sdclem2  37749  heibor1lem  37816  iss2  38345  omabs2  43345  cotrintab  43627  tgblthelfgott  47802  setrec1lem2  49207
  Copyright terms: Public domain W3C validator