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  694  axc16gALT  2520  rspc2vd  3898  trintss  5223  onfununi  8306  smoiun  8326  findcard2  9127  findcard3  9221  inficl  9365  en3lplem2  9562  infxpenlem  9963  alephordi  10024  cardaleph  10039  pwsdompw  10153  cfslb2n  10219  isf32lem10  10313  axdc4lem  10406  zorn2lem2  10448  alephreg  10534  inar1  10727  tskuni  10735  grudomon  10769  nqereu  10881  leltletr  11268  ltleletr  11270  elfz0ubfz0  13631  ssnn0fi  13992  caubnd  15377  sqreulem  15378  bezoutlem1  16564  rppwr  16585  pcprendvds  16867  prmreclem3  16945  ptcmpfi  23861  ufilen  23978  fcfnei  24083  bcthlem5  25378  aaliou  26390  bdayfinbndlem1  28548  wlkres  29826  wlkiswwlks2  30032  3cyclfrgrrn1  30444  n4cyclfrgr  30450  occon2  31448  occon3  31457  atexch  32541  dfufd2lem  33706  sigaclci  34390  onvfowev  35420  fisshasheq  35426  pfxwlk  35435  cusgr3cyclex  35447  idinside  36395  exrecfnlem  37834  poimirlem32  38112  heibor1lem  38269  axc16g-o  39519  axc11-o  39536  aomclem2  43593  frege124d  44298  tratrb  45073  trsspwALT2  45355