Theorem sylcom 31

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 15	. 2 ⊢ ((𝜓 → 𝜒) → (𝜓 → 𝜃))
4	1, 3	syl 18	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl5com  32  syl6  36  syli  40  pm2.18d  128  mpbidi  244  2eu6  2682  dmcosseq  5960  dmcosseqOLD  5961  iss  6027  funopg  6574  funopsn  7151  limuni3  7863  frxp  8138  tz7.49  8455  dif1ennnALT  9268  frfi  9276  unblem3  9286  isfinite2  9290  iunfi  9332  tcrank  9901  setrec1lem2  9967  infdif  10286  isf34lem6  10458  axdc3lem4  10531  suplem1pr  11137  uzwo  13038  gsumcom2  20189  cmpsublem  23717  nrmhaus  24145  metrest  24843  finiunmbl  25865  h1datomi  32183  chirredlem1  32992  fnrelpredd  35720  r1omhfb  35738  r1omhfbregs  35805  onprcf1acwevdlem1  35895  mclsax  36334  antnestlaw2  36457  lineext  36841  in-ax8  37013  ss-ax8  37014  onsucconni  37225  dfttc4  37318  cbveud  38295  sdclem2  38676  heibor1lem  38743  iss2  39276  omabs2  44333  cotrintab  44613  tgblthelfgott  48912