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

Step	Hyp	Ref	Expression
1		sylcom.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylcom.2	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
3	2	a2i 14	. 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃))
4	1, 3	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  241  2eu6  2657  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  iss  5994  funopg  6526  limuni3  7794  frxp  8068  tz7.49  8376  dif1ennnALT  9177  frfi  9185  unblem3  9194  isfinite2  9198  iunfi  9243  tcrank  9796  infdif  10118  isf34lem6  10290  axdc3lem4  10363  suplem1pr  10963  uzwo  12824  gsumcom2  19904  cmpsublem  23343  nrmhaus  23770  metrest  24468  finiunmbl  25501  h1datomi  31656  chirredlem1  32465  fnrelpredd  35247  r1omhfb  35268  r1omhfbregs  35293  mclsax  35763  antnestlaw2  35886  lineext  36270  in-ax8  36418  ss-ax8  36419  onsucconni  36631  cbveud  37573  sdclem2  37939  heibor1lem  38006  iss2  38533  omabs2  43570  cotrintab  43851  tgblthelfgott  48057  setrec1lem2  49929