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  2658  r19.12OLD  3258  dmcosseq  5882  iss  5943  funopg  6468  limuni3  7699  frxp  7967  wfrlem12OLD  8151  tz7.49  8276  dif1enALT  9050  enp1i  9052  frfi  9059  unblem3  9068  isfinite2  9072  iunfi  9107  tcrank  9642  infdif  9965  isf34lem6  10136  axdc3lem4  10209  suplem1pr  10808  uzwo  12651  gsumcom2  19576  cmpsublem  22550  nrmhaus  22977  metrest  23680  finiunmbl  24708  h1datomi  29943  chirredlem1  30752  fnrelpredd  33061  mclsax  33531  lineext  34378  onsucconni  34626  cbveud  35543  sdclem2  35900  heibor1lem  35967  iss2  36479  cotrintab  41222  tgblthelfgott  45267  setrec1lem2  46394