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  2660  r19.12OLD  3321  dmcosseq  5999  dmcosseqOLD  6000  iss  6064  funopg  6612  limuni3  7889  frxp  8167  wfrlem12OLD  8376  tz7.49  8501  dif1ennnALT  9339  enp1iOLD  9342  frfi  9349  unblem3  9358  isfinite2  9362  iunfi  9411  tcrank  9953  infdif  10277  isf34lem6  10449  axdc3lem4  10522  suplem1pr  11121  uzwo  12976  gsumcom2  20017  cmpsublem  23428  nrmhaus  23855  metrest  24558  finiunmbl  25598  h1datomi  31613  chirredlem1  32422  fnrelpredd  35065  mclsax  35537  lineext  36040  in-ax8  36190  ss-ax8  36191  onsucconni  36403  cbveud  37338  sdclem2  37702  heibor1lem  37769  iss2  38300  omabs2  43294  cotrintab  43576  tgblthelfgott  47689  setrec1lem2  48780