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  244  2eu6  2719  r19.12  3283  dmcosseq  5809  iss  5870  funopg  6358  limuni3  7547  frxp  7803  wfrlem12  7949  tz7.49  8064  dif1en  8735  enp1i  8737  frfi  8747  unblem3  8756  isfinite2  8760  iunfi  8796  tcrank  9297  infdif  9620  isf34lem6  9791  axdc3lem4  9864  suplem1pr  10463  uzwo  12299  gsumcom2  19088  cmpsublem  22004  nrmhaus  22431  metrest  23131  finiunmbl  24148  h1datomi  29364  chirredlem1  30173  fnrelpredd  32472  mclsax  32929  lineext  33650  onsucconni  33898  cbveud  34789  sdclem2  35180  heibor1lem  35247  iss2  35761  cotrintab  40314  tgblthelfgott  44333  setrec1lem2  45218