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  2650  dmcosseq  5940  dmcosseqOLD  5941  iss  6006  funopg  6550  limuni3  7828  frxp  8105  tz7.49  8413  dif1ennnALT  9222  enp1iOLD  9225  frfi  9232  unblem3  9241  isfinite2  9245  iunfi  9294  tcrank  9837  infdif  10161  isf34lem6  10333  axdc3lem4  10406  suplem1pr  11005  uzwo  12870  gsumcom2  19905  cmpsublem  23286  nrmhaus  23713  metrest  24412  finiunmbl  25445  h1datomi  31510  chirredlem1  32319  fnrelpredd  35079  mclsax  35556  antnestlaw2  35679  lineext  36064  in-ax8  36212  ss-ax8  36213  onsucconni  36425  cbveud  37360  sdclem2  37736  heibor1lem  37803  iss2  38326  omabs2  43321  cotrintab  43603  tgblthelfgott  47816  setrec1lem2  49677