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  2681  dmcosseq  5959  dmcosseqOLD  5960  iss  6026  funopg  6574  funopsn  7151  limuni3  7863  frxp  8140  tz7.49  8458  dif1ennnALT  9271  frfi  9279  unblem3  9289  isfinite2  9293  iunfi  9335  tcrank  9904  setrec1lem2  9970  infdif  10289  isf34lem6  10461  axdc3lem4  10534  suplem1pr  11140  uzwo  13041  gsumcom2  20194  cmpsublem  23722  nrmhaus  24150  metrest  24848  finiunmbl  25870  h1datomi  32188  chirredlem1  32997  fnrelpredd  35772  r1omhfb  35790  r1omhfbregs  35861  onprcf1acwevdlem1  35964  mclsax  36420  antnestlaw2  36543  lineext  36933  in-ax8  37105  ss-ax8  37106  onsucconni  37317  dfttc4  37410  cbveud  38388  sdclem2  38769  heibor1lem  38836  iss2  39369  omabs2  44427  cotrintab  44707  tgblthelfgott  49006