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  243  2eu6  2740  r19.12  3324  dmcosseq  5838  iss  5897  funopg  6383  limuni3  7561  frxp  7814  wfrlem12  7960  tz7.49  8075  dif1en  8745  enp1i  8747  frfi  8757  unblem3  8766  isfinite2  8770  iunfi  8806  tcrank  9307  infdif  9625  isf34lem6  9796  axdc3lem4  9869  suplem1pr  10468  uzwo  12305  gsumcom2  19089  cmpsublem  22001  nrmhaus  22428  metrest  23128  finiunmbl  24139  h1datomi  29352  chirredlem1  30161  mclsax  32811  lineext  33532  onsucconni  33780  cbveud  34647  sdclem2  35011  heibor1lem  35081  iss2  35595  cotrintab  39967  tgblthelfgott  43974  setrec1lem2  44785