Theorem sylsyld 61

Description: A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
sylsyld.1	⊢ (𝜑 → 𝜓)
sylsyld.2	⊢ (𝜑 → (𝜒 → 𝜃))
sylsyld.3	⊢ (𝜓 → (𝜃 → 𝜏))

Assertion

Ref	Expression
sylsyld	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem sylsyld

Step	Hyp	Ref	Expression
1		sylsyld.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
2		sylsyld.1	. . 3 ⊢ (𝜑 → 𝜓)
3		sylsyld.3	. . 3 ⊢ (𝜓 → (𝜃 → 𝜏))
4	2, 3	syl 17	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	1, 4	syld 47	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:  mpsylsyld  69  syl6an  684  axc16gALT  2493  rspc2vd  3849  trintss  5163  onfununi  8056  smoiun  8076  findcard2  8820  findcard2OLD  8891  findcard3  8892  inficl  9019  en3lplem2  9206  infxpenlem  9592  alephordi  9653  cardaleph  9668  pwsdompw  9783  cfslb2n  9847  isf32lem10  9941  axdc4lem  10034  zorn2lem2  10076  alephreg  10161  inar1  10354  tskuni  10362  grudomon  10396  nqereu  10508  ltleletr  10890  elfz0ubfz0  13181  ssnn0fi  13523  caubnd  14887  sqreulem  14888  bezoutlem1  16062  rppwr  16084  pcprendvds  16356  prmreclem3  16434  ptcmpfi  22664  ufilen  22781  fcfnei  22886  bcthlem5  24179  aaliou  25185  wlkres  27712  wlkiswwlks2  27913  3cyclfrgrrn1  28322  n4cyclfrgr  28328  occon2  29323  occon3  29332  atexch  30416  sigaclci  31766  fisshasheq  32740  pfxwlk  32752  cusgr3cyclex  32765  frmin  33459  idinside  34072  exrecfnlem  35236  poimirlem32  35495  heibor1lem  35653  axc16g-o  36634  axc11-o  36651  aomclem2  40524  frege124d  40987  tratrb  41770  trsspwALT2  42053  leltletr  44401