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  2654  dmcosseq  5921  dmcosseqOLD  5922  dmcosseqOLDOLD  5923  iss  5988  funopg  6520  limuni3  7788  frxp  8062  tz7.49  8370  dif1ennnALT  9168  frfi  9176  unblem3  9185  isfinite2  9189  iunfi  9234  tcrank  9784  infdif  10106  isf34lem6  10278  axdc3lem4  10351  suplem1pr  10950  uzwo  12811  gsumcom2  19889  cmpsublem  23315  nrmhaus  23742  metrest  24440  finiunmbl  25473  h1datomi  31563  chirredlem1  32372  fnrelpredd  35123  r1omhfb  35144  r1omhfbregs  35154  mclsax  35634  antnestlaw2  35757  lineext  36141  in-ax8  36289  ss-ax8  36290  onsucconni  36502  cbveud  37437  sdclem2  37802  heibor1lem  37869  iss2  38396  omabs2  43449  cotrintab  43731  tgblthelfgott  47939  setrec1lem2  49813