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  244  2eu6  2678  r19.12  3248  dmcosseq  5814  iss  5875  funopg  6369  limuni3  7566  frxp  7825  wfrlem12  7976  tz7.49  8091  dif1enOLD  8787  enp1i  8789  frfi  8796  unblem3  8805  isfinite2  8809  iunfi  8845  tcrank  9346  infdif  9669  isf34lem6  9840  axdc3lem4  9913  suplem1pr  10512  uzwo  12351  gsumcom2  19163  cmpsublem  22099  nrmhaus  22526  metrest  23226  finiunmbl  24244  h1datomi  29463  chirredlem1  30272  fnrelpredd  32590  mclsax  33047  lineext  33927  onsucconni  34175  cbveud  35069  sdclem2  35460  heibor1lem  35527  iss2  36041  cotrintab  40687  tgblthelfgott  44700  setrec1lem2  45609
 Copyright terms: Public domain W3C validator