Theorem sylcom 31

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 15	. 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃))
4	1, 3	syl 18	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl5com  32  syl6  36  syli  40  pm2.18d  128  mpbidi  244  2eu6  2684  dmcosseq  5967  dmcosseqOLD  5968  iss  6039  funopg  6594  funopsn  7175  limuni3  7887  frxp  8165  tz7.49  8483  dif1ennnALT  9296  frfi  9304  unblem3  9314  isfinite2  9318  iunfi  9360  tcrank  9928  setrec1lem2  9994  infdif  10313  isf34lem6  10485  axdc3lem4  10558  suplem1pr  11164  uzwo  13065  gsumcom2  20219  cmpsublem  23747  nrmhaus  24175  metrest  24873  finiunmbl  25895  h1datomi  32213  chirredlem1  33022  fnrelpredd  35804  eqhf  35820  eqhfregs  35905  onprcf1acwevdlem1  36045  mclsax  36501  antnestlaw2  36624  lineext  37019  in-ax8  37191  ss-ax8  37192  onsucconni  37403  dfttc4  37496  cbveud  38487  sdclem2  38868  heibor1lem  38935  iss2  39468  omabs2  44526  cotrintab  44806  tgblthelfgott  49118