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  mpbidi  231  2eu6  2558  dmcosseq  5387  iss  5447  funopg  5922  limuni3  7052  frxp  7287  wfrlem12  7426  tz7.49  7540  dif1en  8193  enp1i  8195  frfi  8205  unblem3  8214  isfinite2  8218  iunfi  8254  tcrank  8747  infdif  9031  isf34lem6  9202  axdc3lem4  9275  suplem1pr  9874  uzwo  11751  gsumcom2  18374  cmpsublem  21202  nrmhaus  21629  metrest  22329  finiunmbl  23312  h1datomi  28440  chirredlem1  29249  mclsax  31466  frrlem11  31792  lineext  32183  onsucconni  32436  bj-ismooredr2  33065  sdclem2  33538  heibor1lem  33608  iss2  34112  cotrintab  37921  tgblthelfgott  41703  tgblthelfgottOLD  41709  setrec1lem2  42435