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  2653  r19.12OLD  3313  dmcosseq  5971  iss  6034  funopg  6580  limuni3  7838  frxp  8109  wfrlem12OLD  8317  tz7.49  8442  dif1ennnALT  9274  enp1iOLD  9277  frfi  9285  unblem3  9294  isfinite2  9298  iunfi  9337  tcrank  9876  infdif  10201  isf34lem6  10372  axdc3lem4  10445  suplem1pr  11044  uzwo  12892  gsumcom2  19838  cmpsublem  22895  nrmhaus  23322  metrest  24025  finiunmbl  25053  h1datomi  30822  chirredlem1  31631  fnrelpredd  34081  mclsax  34549  lineext  35037  onsucconni  35311  cbveud  36242  sdclem2  36599  heibor1lem  36666  iss2  37202  omabs2  42068  cotrintab  42351  tgblthelfgott  46470  setrec1lem2  47687