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 ⊢ (𝜑 → (𝜒 → 𝜏))

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  70  syl6an  696  axc16gALT  2528  rspc2vd  3909  trintss  5238  onfununi  8324  smoiun  8344  findcard2  9145  findcard3  9239  inficl  9381  en3lplem2  9578  infxpenlem  9993  alephordi  10054  cardaleph  10069  pwsdompw  10182  cfslb2n  10248  isf32lem10  10342  axdc4lem  10435  zorn2lem2  10477  alephreg  10563  inar1  10756  tskuni  10764  grudomon  10798  nqereu  10910  leltletr  11297  ltleletr  11299  elfz0ubfz0  13656  ssnn0fi  14017  caubnd  15406  sqreulem  15407  bezoutlem1  16593  rppwr  16614  pcprendvds  16896  prmreclem3  16974  ptcmpfi  23935  ufilen  24052  fcfnei  24157  bcthlem5  25452  aaliou  26464  bdayfinbndlem1  28622  wlkres  29955  wlkiswwlks2  30161  3cyclfrgrrn1  30573  n4cyclfrgr  30579  occon2  31577  occon3  31586  atexch  32670  dfufd2lem  33780  sigaclci  34463  onvfowev  35495  fisshasheq  35501  pfxwlk  35511  cusgr3cyclex  35523  idinside  36471  exrecfnlem  37908  poimirlem32  38186  heibor1lem  38343  axc16g-o  39593  axc11-o  39610  aomclem2  43667  frege124d  44372  tratrb  45130  trsspwALT2  45412