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  240  2eu6  2658  r19.12OLD  3253  dmcosseq  5871  iss  5932  funopg  6452  limuni3  7674  frxp  7938  wfrlem12OLD  8122  tz7.49  8246  dif1enALT  8980  enp1i  8982  frfi  8989  unblem3  8998  isfinite2  9002  iunfi  9037  tcrank  9573  infdif  9896  isf34lem6  10067  axdc3lem4  10140  suplem1pr  10739  uzwo  12580  gsumcom2  19491  cmpsublem  22458  nrmhaus  22885  metrest  23586  finiunmbl  24613  h1datomi  29844  chirredlem1  30653  fnrelpredd  32961  mclsax  33431  lineext  34305  onsucconni  34553  cbveud  35470  sdclem2  35827  heibor1lem  35894  iss2  36406  cotrintab  41111  tgblthelfgott  45155  setrec1lem2  46280