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  2687  dmcosseq  5973  dmcosseqOLD  5974  iss  6042  funopg  6577  funopsn  7151  limuni3  7857  frxp  8131  tz7.49  8441  dif1ennnALT  9247  frfi  9255  unblem3  9264  isfinite2  9268  iunfi  9310  tcrank  9866  infdif  10210  isf34lem6  10382  axdc3lem4  10455  suplem1pr  11055  uzwo  12953  gsumcom2  20076  cmpsublem  23593  nrmhaus  24020  metrest  24718  finiunmbl  25740  h1datomi  31970  chirredlem1  32779  fnrelpredd  35507  r1omhfb  35533  r1omhfbregs  35574  mclsax  36082  antnestlaw2  36205  lineext  36589  in-ax8  36777  ss-ax8  36778  onsucconni  36989  dfttc4  37082  cbveud  38059  sdclem2  38434  heibor1lem  38501  iss2  39034  omabs2  44100  cotrintab  44381  tgblthelfgott  48621  setrec1lem2  50507