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  240  2eu6  2651  r19.12OLD  3311  dmcosseq  5972  iss  6035  funopg  6582  limuni3  7845  frxp  8117  wfrlem12OLD  8326  tz7.49  8451  dif1ennnALT  9283  enp1iOLD  9286  frfi  9294  unblem3  9303  isfinite2  9307  iunfi  9346  tcrank  9885  infdif  10210  isf34lem6  10381  axdc3lem4  10454  suplem1pr  11053  uzwo  12902  gsumcom2  19891  cmpsublem  23223  nrmhaus  23650  metrest  24353  finiunmbl  25393  h1datomi  31267  chirredlem1  32076  fnrelpredd  34556  mclsax  35024  lineext  35518  onsucconni  35786  cbveud  36717  sdclem2  37074  heibor1lem  37141  iss2  37677  omabs2  42545  cotrintab  42828  tgblthelfgott  46942  setrec1lem2  47895