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  690  axc16gALT  2498  rspc2vd  3886  trintss  5205  onfununi  8278  smoiun  8298  findcard2  9096  findcard3  9190  inficl  9335  en3lplem2  9532  infxpenlem  9933  alephordi  9994  cardaleph  10009  pwsdompw  10123  cfslb2n  10188  isf32lem10  10282  axdc4lem  10375  zorn2lem2  10417  alephreg  10503  inar1  10696  tskuni  10704  grudomon  10738  nqereu  10850  leltletr  11235  ltleletr  11237  elfz0ubfz0  13584  ssnn0fi  13945  caubnd  15319  sqreulem  15320  bezoutlem1  16506  rppwr  16527  pcprendvds  16809  prmreclem3  16887  ptcmpfi  23803  ufilen  23920  fcfnei  24025  bcthlem5  25320  aaliou  26329  bdayfinbndlem1  28484  wlkres  29762  wlkiswwlks2  29968  3cyclfrgrrn1  30380  n4cyclfrgr  30386  occon2  31384  occon3  31393  atexch  32477  dfufd2lem  33639  sigaclci  34323  fisshasheq  35350  pfxwlk  35359  cusgr3cyclex  35371  idinside  36319  exrecfnlem  37748  poimirlem32  38026  heibor1lem  38183  axc16g-o  39433  axc11-o  39450  aomclem2  43507  frege124d  44212  tratrb  44987  trsspwALT2  45269