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  2650  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  iss  5990  funopg  6520  limuni3  7792  frxp  8066  tz7.49  8374  dif1ennnALT  9180  enp1iOLD  9183  frfi  9190  unblem3  9199  isfinite2  9203  iunfi  9252  tcrank  9799  infdif  10121  isf34lem6  10293  axdc3lem4  10366  suplem1pr  10965  uzwo  12830  gsumcom2  19872  cmpsublem  23302  nrmhaus  23729  metrest  24428  finiunmbl  25461  h1datomi  31543  chirredlem1  32352  fnrelpredd  35055  mclsax  35541  antnestlaw2  35664  lineext  36049  in-ax8  36197  ss-ax8  36198  onsucconni  36410  cbveud  37345  sdclem2  37721  heibor1lem  37788  iss2  38311  omabs2  43305  cotrintab  43587  tgblthelfgott  47800  setrec1lem2  49674