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  2656  dmcosseq  5956  dmcosseqOLD  5957  iss  6022  funopg  6570  limuni3  7847  frxp  8125  wfrlem12OLD  8334  tz7.49  8459  dif1ennnALT  9283  enp1iOLD  9286  frfi  9293  unblem3  9302  isfinite2  9306  iunfi  9355  tcrank  9898  infdif  10222  isf34lem6  10394  axdc3lem4  10467  suplem1pr  11066  uzwo  12927  gsumcom2  19956  cmpsublem  23337  nrmhaus  23764  metrest  24463  finiunmbl  25497  h1datomi  31562  chirredlem1  32371  fnrelpredd  35120  mclsax  35591  lineext  36094  in-ax8  36242  ss-ax8  36243  onsucconni  36455  cbveud  37390  sdclem2  37766  heibor1lem  37833  iss2  38362  omabs2  43356  cotrintab  43638  tgblthelfgott  47829  setrec1lem2  49552