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  241  2eu6  2655  r19.12OLD  3313  dmcosseq  5990  dmcosseqOLD  5991  iss  6055  funopg  6602  limuni3  7873  frxp  8150  wfrlem12OLD  8359  tz7.49  8484  dif1ennnALT  9309  enp1iOLD  9312  frfi  9319  unblem3  9328  isfinite2  9332  iunfi  9381  tcrank  9922  infdif  10246  isf34lem6  10418  axdc3lem4  10491  suplem1pr  11090  uzwo  12951  gsumcom2  20008  cmpsublem  23423  nrmhaus  23850  metrest  24553  finiunmbl  25593  h1datomi  31610  chirredlem1  32419  fnrelpredd  35082  mclsax  35554  lineext  36058  in-ax8  36207  ss-ax8  36208  onsucconni  36420  cbveud  37355  sdclem2  37729  heibor1lem  37796  iss2  38326  omabs2  43322  cotrintab  43604  tgblthelfgott  47740  setrec1lem2  48919