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  242  2eu6  2661  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  iss  5994  funopg  6526  funopsn  7097  limuni3  7799  frxp  8073  tz7.49  8381  dif1ennnALT  9184  frfi  9192  unblem3  9201  isfinite2  9205  iunfi  9250  tcrank  9806  infdif  10128  isf34lem6  10300  axdc3lem4  10373  suplem1pr  10973  uzwo  12859  gsumcom2  19948  cmpsublem  23389  nrmhaus  23816  metrest  24514  finiunmbl  25536  h1datomi  31677  chirredlem1  32486  fnrelpredd  35279  r1omhfb  35300  r1omhfbregs  35325  mclsax  35804  antnestlaw2  35927  lineext  36311  in-ax8  36459  ss-ax8  36460  onsucconni  36672  dfttc4  36765  cbveud  37741  sdclem2  38116  heibor1lem  38183  iss2  38718  omabs2  43784  cotrintab  44065  tgblthelfgott  48313  setrec1lem2  50185