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  2683  dmcosseq  5966  dmcosseqOLD  5967  iss  6035  funopg  6571  funopsn  7148  limuni3  7852  frxp  8128  tz7.49  8438  dif1ennnALT  9251  frfi  9259  unblem3  9268  isfinite2  9272  iunfi  9314  tcrank  9870  infdif  10214  isf34lem6  10386  axdc3lem4  10459  suplem1pr  11065  uzwo  12964  gsumcom2  20108  cmpsublem  23630  nrmhaus  24058  metrest  24756  finiunmbl  25778  h1datomi  32070  chirredlem1  32879  fnrelpredd  35604  r1omhfb  35630  r1omhfbregs  35671  mclsax  36156  antnestlaw2  36279  lineext  36664  in-ax8  36852  ss-ax8  36853  onsucconni  37064  dfttc4  37157  cbveud  38134  sdclem2  38500  heibor1lem  38567  iss2  39100  omabs2  44181  cotrintab  44462  tgblthelfgott  48739  setrec1lem2  50622