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  240  2eu6  2653  r19.12OLD  3313  dmcosseq  5967  iss  6028  funopg  6574  limuni3  7828  frxp  8099  wfrlem12OLD  8307  tz7.49  8432  dif1ennnALT  9265  enp1iOLD  9268  frfi  9276  unblem3  9285  isfinite2  9289  iunfi  9328  tcrank  9866  infdif  10191  isf34lem6  10362  axdc3lem4  10435  suplem1pr  11034  uzwo  12882  gsumcom2  19826  cmpsublem  22872  nrmhaus  23299  metrest  24002  finiunmbl  25030  h1datomi  30799  chirredlem1  31608  fnrelpredd  34023  mclsax  34491  lineext  34979  onsucconni  35227  cbveud  36158  sdclem2  36516  heibor1lem  36583  iss2  37119  omabs2  41953  cotrintab  42236  tgblthelfgott  46356  setrec1lem2  47573
  Copyright terms: Public domain W3C validator