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  2490  rspc2vd  3898  trintss  5216  onfununi  8261  smoiun  8281  findcard2  9074  findcard3  9167  inficl  9309  en3lplem2  9503  infxpenlem  9904  alephordi  9965  cardaleph  9980  pwsdompw  10094  cfslb2n  10159  isf32lem10  10253  axdc4lem  10346  zorn2lem2  10388  alephreg  10473  inar1  10666  tskuni  10674  grudomon  10708  nqereu  10820  leltletr  11204  ltleletr  11206  elfz0ubfz0  13532  ssnn0fi  13892  caubnd  15266  sqreulem  15267  bezoutlem1  16450  rppwr  16471  pcprendvds  16752  prmreclem3  16830  ptcmpfi  23729  ufilen  23846  fcfnei  23951  bcthlem5  25256  aaliou  26274  wlkres  29648  wlkiswwlks2  29854  3cyclfrgrrn1  30263  n4cyclfrgr  30269  occon2  31266  occon3  31275  atexch  32359  dfufd2lem  33512  sigaclci  34143  fisshasheq  35157  pfxwlk  35166  cusgr3cyclex  35178  idinside  36124  exrecfnlem  37419  poimirlem32  37698  heibor1lem  37855  axc16g-o  38979  axc11-o  38996  aomclem2  43094  frege124d  43800  tratrb  44575  trsspwALT2  44857