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  3893  trintss  5214  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  23728  ufilen  23845  fcfnei  23950  bcthlem5  25255  aaliou  26273  wlkres  29647  wlkiswwlks2  29853  3cyclfrgrrn1  30265  n4cyclfrgr  30271  occon2  31268  occon3  31277  atexch  32361  dfufd2lem  33514  sigaclci  34145  fisshasheq  35159  pfxwlk  35168  cusgr3cyclex  35180  idinside  36128  exrecfnlem  37423  poimirlem32  37691  heibor1lem  37848  axc16g-o  39032  axc11-o  39049  aomclem2  43147  frege124d  43853  tratrb  44628  trsspwALT2  44910