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  683  axc16gALT  2490  rspc2vd  3945  trintss  5285  onfununi  8341  smoiun  8361  findcard2  9164  findcard2OLD  9284  findcard3  9285  findcard3OLD  9286  inficl  9420  en3lplem2  9608  infxpenlem  10008  alephordi  10069  cardaleph  10084  pwsdompw  10199  cfslb2n  10263  isf32lem10  10357  axdc4lem  10450  zorn2lem2  10492  alephreg  10577  inar1  10770  tskuni  10778  grudomon  10812  nqereu  10924  leltletr  11305  ltleletr  11307  elfz0ubfz0  13605  ssnn0fi  13950  caubnd  15305  sqreulem  15306  bezoutlem1  16481  rppwr  16501  pcprendvds  16773  prmreclem3  16851  ptcmpfi  23317  ufilen  23434  fcfnei  23539  bcthlem5  24845  aaliou  25851  wlkres  28958  wlkiswwlks2  29160  3cyclfrgrrn1  29569  n4cyclfrgr  29575  occon2  30572  occon3  30581  atexch  31665  sigaclci  33161  fisshasheq  34135  pfxwlk  34145  cusgr3cyclex  34158  idinside  35087  exrecfnlem  36308  poimirlem32  36568  heibor1lem  36725  axc16g-o  37852  axc11-o  37869  aomclem2  41845  frege124d  42560  tratrb  43345  trsspwALT2  43628