Theorem sylsyld 62

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 18	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	1, 4	syld 48	1 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpsylsyld  70  syl6an  697  axc16gALT  2522  rspc2vd  3899  trintss  5237  onfununi  8387  smoiun  8407  findcard2  9218  findcard3  9312  inficl  9454  en3lplem2  9651  infxpenlem  10131  alephordi  10192  cardaleph  10207  pwsdompw  10320  cfslb2n  10385  isf32lem10  10479  axdc4lem  10572  zorn2lem2  10614  alephreg  10706  inar1  10899  tskuni  10907  grudomon  10941  nqereu  11053  leltletr  11440  ltleletr  11442  elfz0ubfz0  13806  ssnn0fi  14168  caubnd  15570  sqreulem  15571  bezoutlem1  16756  rppwr  16778  pcprendvds  17062  prmreclem3  17140  ptcmpfi  24187  ufilen  24304  fcfnei  24409  bcthlem5  25704  aaliou  26722  bdayfinbndlem1  28910  wlkres  30306  pfxwlk  30323  wlkiswwlks2  30521  3cyclfrgrrn1  30943  n4cyclfrgr  30949  occon2  31947  occon3  31956  atexch  33040  dfufd2lem  34185  sigaclci  34875  onvfowev  36091  onprcf1of1orbd  36095  fisshasheq  36101  cusgr3cyclex  36109  idinside  37064  exrecfnlem  38570  poimirlem32  38838  heibor1lem  39009  axc16g-o  40257  axc11-o  40274  aomclem2  44323  frege124d  45022  tratrb  45779  trsspwALT2  46061