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  mpbidi  231  2eu6  2556  dmcosseq  5376  iss  5435  funopg  5910  limuni3  7037  frxp  7272  wfrlem12  7411  tz7.49  7525  dif1en  8178  enp1i  8180  frfi  8190  unblem3  8199  isfinite2  8203  iunfi  8239  tcrank  8732  infdif  9016  isf34lem6  9187  axdc3lem4  9260  suplem1pr  9859  uzwo  11736  gsumcom2  18355  cmpsublem  21183  nrmhaus  21610  metrest  22310  finiunmbl  23293  h1datomi  28410  chirredlem1  29219  mclsax  31440  frrlem11  31766  lineext  32158  onsucconni  32411  bj-ismooredr2  33040  sdclem2  33509  heibor1lem  33579  cotrintab  37740  tgblthelfgott  41468  tgblthelfgottOLD  41474  setrec1lem2  42200
 Copyright terms: Public domain W3C validator