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  2651  dmcosseq  5943  dmcosseqOLD  5944  iss  6009  funopg  6553  limuni3  7831  frxp  8108  tz7.49  8416  dif1ennnALT  9229  enp1iOLD  9232  frfi  9239  unblem3  9248  isfinite2  9252  iunfi  9301  tcrank  9844  infdif  10168  isf34lem6  10340  axdc3lem4  10413  suplem1pr  11012  uzwo  12877  gsumcom2  19912  cmpsublem  23293  nrmhaus  23720  metrest  24419  finiunmbl  25452  h1datomi  31517  chirredlem1  32326  fnrelpredd  35086  mclsax  35563  antnestlaw2  35686  lineext  36071  in-ax8  36219  ss-ax8  36220  onsucconni  36432  cbveud  37367  sdclem2  37743  heibor1lem  37810  iss2  38333  omabs2  43328  cotrintab  43610  tgblthelfgott  47820  setrec1lem2  49681