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  242  2eu6  2742  r19.12  3328  dmcosseq  5842  iss  5901  funopg  6385  limuni3  7558  frxp  7814  wfrlem12  7960  tz7.49  8075  dif1en  8743  enp1i  8745  frfi  8755  unblem3  8764  isfinite2  8768  iunfi  8804  tcrank  9305  infdif  9623  isf34lem6  9794  axdc3lem4  9867  suplem1pr  10466  uzwo  12303  gsumcom2  19017  cmpsublem  21923  nrmhaus  22350  metrest  23049  finiunmbl  24060  h1datomi  29272  chirredlem1  30081  mclsax  32700  lineext  33421  onsucconni  33669  cbveud  34522  sdclem2  34885  heibor1lem  34955  iss2  35469  cotrintab  39835  tgblthelfgott  43808  setrec1lem2  44619
  Copyright terms: Public domain W3C validator