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  232  2eu6  2722  dmcosseq  5588  iss  5652  funopg  6135  limuni3  7282  frxp  7521  wfrlem12  7662  tz7.49  7776  dif1en  8432  enp1i  8434  frfi  8444  unblem3  8453  isfinite2  8457  iunfi  8493  tcrank  8994  infdif  9316  isf34lem6  9487  axdc3lem4  9560  suplem1pr  10159  uzwo  11970  gsumcom2  18575  cmpsublem  21416  nrmhaus  21843  metrest  22542  finiunmbl  23525  h1datomi  28768  chirredlem1  29577  mclsax  31789  lineext  32504  onsucconni  32753  bj-ismooredr2  33376  sdclem2  33849  heibor1lem  33919  iss2  34425  cotrintab  38421  tgblthelfgott  42278  setrec1lem2  43003
  Copyright terms: Public domain W3C validator