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  2652  dmcosseq  5917  dmcosseqOLD  5918  dmcosseqOLDOLD  5919  iss  5984  funopg  6515  limuni3  7782  frxp  8056  tz7.49  8364  dif1ennnALT  9161  frfi  9169  unblem3  9178  isfinite2  9182  iunfi  9227  tcrank  9774  infdif  10096  isf34lem6  10268  axdc3lem4  10341  suplem1pr  10940  uzwo  12806  gsumcom2  19885  cmpsublem  23312  nrmhaus  23739  metrest  24437  finiunmbl  25470  h1datomi  31556  chirredlem1  32365  fnrelpredd  35097  r1omhfbregs  35121  mclsax  35601  antnestlaw2  35724  lineext  36109  in-ax8  36257  ss-ax8  36258  onsucconni  36470  cbveud  37405  sdclem2  37781  heibor1lem  37848  iss2  38371  omabs2  43364  cotrintab  43646  tgblthelfgott  47845  setrec1lem2  49719