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  2657  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  iss  6000  funopg  6532  funopsn  7101  limuni3  7803  frxp  8076  tz7.49  8384  dif1ennnALT  9187  frfi  9195  unblem3  9204  isfinite2  9208  iunfi  9253  tcrank  9808  infdif  10130  isf34lem6  10302  axdc3lem4  10375  suplem1pr  10975  uzwo  12861  gsumcom2  19950  cmpsublem  23364  nrmhaus  23791  metrest  24489  finiunmbl  25511  h1datomi  31652  chirredlem1  32461  fnrelpredd  35234  r1omhfb  35256  r1omhfbregs  35281  mclsax  35751  antnestlaw2  35874  lineext  36258  in-ax8  36406  ss-ax8  36407  onsucconni  36619  dfttc4  36712  cbveud  37688  sdclem2  38063  heibor1lem  38130  iss2  38665  omabs2  43760  cotrintab  44041  tgblthelfgott  48291  setrec1lem2  50163