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  34  syli  38  mpbidi  229  2eu6  2541  dmcosseq  5291  iss  5350  funopg  5818  limuni3  6917  frxp  7147  wfrlem12  7286  tz7.49  7400  dif1en  8051  enp1i  8053  frfi  8063  unblem3  8072  isfinite2  8076  iunfi  8110  tcrank  8603  infdif  8887  isf34lem6  9058  axdc3lem4  9131  suplem1pr  9726  uzwo  11579  gsumcom2  18139  cmpsublem  20950  nrmhaus  21377  metrest  22076  finiunmbl  23032  wilthlem3  24509  cusgrafi  25772  clwwlkn0  26064  h1datomi  27626  chirredlem1  28435  mclsax  30522  frrlem11  30838  lineext  31155  onsucconi  31408  sdclem2  32507  heibor1lem  32577  cotrintab  36739  tgblthelfgott  40030  tgblthelfgottOLD  40037
  Copyright terms: Public domain W3C validator