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  2650  r19.12OLD  3310  dmcosseq  5971  iss  6034  funopg  6581  limuni3  7843  frxp  8114  wfrlem12OLD  8322  tz7.49  8447  dif1ennnALT  9279  enp1iOLD  9282  frfi  9290  unblem3  9299  isfinite2  9303  iunfi  9342  tcrank  9881  infdif  10206  isf34lem6  10377  axdc3lem4  10450  suplem1pr  11049  uzwo  12899  gsumcom2  19884  cmpsublem  23123  nrmhaus  23550  metrest  24253  finiunmbl  25293  h1datomi  31101  chirredlem1  31910  fnrelpredd  34390  mclsax  34858  lineext  35352  onsucconni  35625  cbveud  36556  sdclem2  36913  heibor1lem  36980  iss2  37516  omabs2  42384  cotrintab  42667  tgblthelfgott  46781  setrec1lem2  47820