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  mpbidi  231  2eu6  2696  dmcosseq  5542  iss  5605  funopg  6083  limuni3  7218  frxp  7456  wfrlem12  7596  tz7.49  7710  dif1en  8360  enp1i  8362  frfi  8372  unblem3  8381  isfinite2  8385  iunfi  8421  tcrank  8922  infdif  9243  isf34lem6  9414  axdc3lem4  9487  suplem1pr  10086  uzwo  11964  gsumcom2  18594  cmpsublem  21424  nrmhaus  21851  metrest  22550  finiunmbl  23532  h1datomi  28770  chirredlem1  29579  mclsax  31794  lineext  32510  onsucconni  32763  bj-ismooredr2  33389  sdclem2  33869  heibor1lem  33939  iss2  34453  cotrintab  38441  tgblthelfgott  42231  tgblthelfgottOLD  42237  setrec1lem2  42963
  Copyright terms: Public domain W3C validator