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  3895  trintss  5231  onfununi  8330  smoiun  8350  findcard2  9159  findcard3  9253  inficl  9395  en3lplem2  9592  infxpenlem  10016  alephordi  10077  cardaleph  10092  pwsdompw  10205  cfslb2n  10270  isf32lem10  10364  axdc4lem  10457  zorn2lem2  10499  alephreg  10591  inar1  10784  tskuni  10792  grudomon  10826  nqereu  10938  leltletr  11325  ltleletr  11327  elfz0ubfz0  13687  ssnn0fi  14049  caubnd  15446  sqreulem  15447  bezoutlem1  16629  rppwr  16650  pcprendvds  16932  prmreclem3  17010  ptcmpfi  24039  ufilen  24156  fcfnei  24261  bcthlem5  25556  aaliou  26574  bdayfinbndlem1  28732  wlkres  30128  pfxwlk  30145  wlkiswwlks2  30343  3cyclfrgrrn1  30765  n4cyclfrgr  30771  occon2  31769  occon3  31778  atexch  32862  dfufd2lem  33959  sigaclci  34642  onvfowev  35713  fisshasheq  35717  cusgr3cyclex  35725  idinside  36664  exrecfnlem  38133  poimirlem32  38401  heibor1lem  38559  axc16g-o  39807  axc11-o  39824  aomclem2  43896  frege124d  44601  tratrb  45359  trsspwALT2  45641