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  2658  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  iss  6002  funopg  6534  limuni3  7804  frxp  8078  tz7.49  8386  dif1ennnALT  9189  frfi  9197  unblem3  9206  isfinite2  9210  iunfi  9255  tcrank  9808  infdif  10130  isf34lem6  10302  axdc3lem4  10375  suplem1pr  10975  uzwo  12836  gsumcom2  19916  cmpsublem  23355  nrmhaus  23782  metrest  24480  finiunmbl  25513  h1datomi  31668  chirredlem1  32477  fnrelpredd  35266  r1omhfb  35287  r1omhfbregs  35312  mclsax  35782  antnestlaw2  35905  lineext  36289  in-ax8  36437  ss-ax8  36438  onsucconni  36650  cbveud  37621  sdclem2  37987  heibor1lem  38054  iss2  38589  omabs2  43683  cotrintab  43964  tgblthelfgott  48169  setrec1lem2  50041