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  2519  rspc2vd  3894  trintss  5230  onfununi  8353  smoiun  8373  findcard2  9184  findcard3  9278  inficl  9421  en3lplem2  9618  infxpenlem  10096  alephordi  10157  cardaleph  10172  pwsdompw  10285  cfslb2n  10350  isf32lem10  10444  axdc4lem  10537  zorn2lem2  10579  alephreg  10671  inar1  10864  tskuni  10872  grudomon  10906  nqereu  11018  leltletr  11405  ltleletr  11407  elfz0ubfz0  13770  ssnn0fi  14132  caubnd  15532  sqreulem  15533  bezoutlem1  16718  rppwr  16740  pcprendvds  17024  prmreclem3  17102  ptcmpfi  24138  ufilen  24255  fcfnei  24360  bcthlem5  25655  aaliou  26671  bdayfinbndlem1  28859  wlkres  30255  pfxwlk  30272  wlkiswwlks2  30470  3cyclfrgrrn1  30892  n4cyclfrgr  30898  occon2  31896  occon3  31905  atexch  32989  dfufd2lem  34128  sigaclci  34811  onvfowev  35970  onprcf1of1orbd  35974  fisshasheq  35980  cusgr3cyclex  35988  idinside  36942  exrecfnlem  38396  poimirlem32  38664  heibor1lem  38837  axc16g-o  40085  axc11-o  40102  aomclem2  44151  frege124d  44855  tratrb  45613  trsspwALT2  45895