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  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  iss  5994  funopg  6526  limuni3  7796  frxp  8069  tz7.49  8377  dif1ennnALT  9180  frfi  9188  unblem3  9197  isfinite2  9201  iunfi  9246  tcrank  9799  infdif  10121  isf34lem6  10293  axdc3lem4  10366  suplem1pr  10966  uzwo  12852  gsumcom2  19941  cmpsublem  23374  nrmhaus  23801  metrest  24499  finiunmbl  25521  h1datomi  31667  chirredlem1  32476  fnrelpredd  35250  r1omhfb  35272  r1omhfbregs  35297  mclsax  35767  antnestlaw2  35890  lineext  36274  in-ax8  36422  ss-ax8  36423  onsucconni  36635  dfttc4  36728  cbveud  37702  sdclem2  38077  heibor1lem  38144  iss2  38679  omabs2  43778  cotrintab  44059  tgblthelfgott  48303  setrec1lem2  50175