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  243  2eu6  2742  r19.12  3326  dmcosseq  5846  iss  5905  funopg  6391  limuni3  7569  frxp  7822  wfrlem12  7968  tz7.49  8083  dif1en  8753  enp1i  8755  frfi  8765  unblem3  8774  isfinite2  8778  iunfi  8814  tcrank  9315  infdif  9633  isf34lem6  9804  axdc3lem4  9877  suplem1pr  10476  uzwo  12314  gsumcom2  19097  cmpsublem  22009  nrmhaus  22436  metrest  23136  finiunmbl  24147  h1datomi  29360  chirredlem1  30169  mclsax  32818  lineext  33539  onsucconni  33787  cbveud  34655  sdclem2  35019  heibor1lem  35089  iss2  35603  cotrintab  39981  tgblthelfgott  43987  setrec1lem2  44798