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  682  axc16gALT  2493  rspc2vd  3898  trintss  5233  onfununi  8247  smoiun  8267  findcard2  9034  findcard2OLD  9154  findcard3  9155  findcard3OLD  9156  inficl  9287  en3lplem2  9475  infxpenlem  9875  alephordi  9936  cardaleph  9951  pwsdompw  10066  cfslb2n  10130  isf32lem10  10224  axdc4lem  10317  zorn2lem2  10359  alephreg  10444  inar1  10637  tskuni  10645  grudomon  10679  nqereu  10791  leltletr  11172  ltleletr  11174  elfz0ubfz0  13466  ssnn0fi  13811  caubnd  15170  sqreulem  15171  bezoutlem1  16347  rppwr  16367  pcprendvds  16639  prmreclem3  16717  ptcmpfi  23070  ufilen  23187  fcfnei  23292  bcthlem5  24598  aaliou  25604  wlkres  28326  wlkiswwlks2  28528  3cyclfrgrrn1  28937  n4cyclfrgr  28943  occon2  29938  occon3  29947  atexch  31031  sigaclci  32396  fisshasheq  33370  pfxwlk  33382  cusgr3cyclex  33395  idinside  34523  exrecfnlem  35704  poimirlem32  35963  heibor1lem  36121  axc16g-o  37250  axc11-o  37267  aomclem2  41192  frege124d  41740  tratrb  42527  trsspwALT2  42810