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  2557  dmcosseq  5357  iss  5416  funopg  5890  limuni3  7014  frxp  7247  wfrlem12  7386  tz7.49  7500  dif1en  8153  enp1i  8155  frfi  8165  unblem3  8174  isfinite2  8178  iunfi  8214  tcrank  8707  infdif  8991  isf34lem6  9162  axdc3lem4  9235  suplem1pr  9834  uzwo  11711  gsumcom2  18314  cmpsublem  21142  nrmhaus  21569  metrest  22269  finiunmbl  23252  h1datomi  28328  chirredlem1  29137  mclsax  31227  frrlem11  31546  lineext  31878  onsucconni  32131  sdclem2  33209  heibor1lem  33279  cotrintab  37441  tgblthelfgott  41020  tgblthelfgottOLD  41027  setrec1lem2  41758
  Copyright terms: Public domain W3C validator