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  682  axc16gALT  2529  rspc2vd  3934  trintss  5191  onfununi  7980  smoiun  8000  findcard2  8760  findcard3  8763  inficl  8891  en3lplem2  9078  infxpenlem  9441  alephordi  9502  cardaleph  9517  pwsdompw  9628  cfslb2n  9692  isf32lem10  9786  axdc4lem  9879  zorn2lem2  9921  alephreg  10006  inar1  10199  tskuni  10207  grudomon  10241  nqereu  10353  ltleletr  10735  elfz0ubfz0  13014  ssnn0fi  13356  caubnd  14720  sqreulem  14721  bezoutlem1  15889  pcprendvds  16179  prmreclem3  16256  ptcmpfi  22423  ufilen  22540  fcfnei  22645  bcthlem5  23933  aaliou  24929  wlkres  27454  wlkiswwlks2  27655  3cyclfrgrrn1  28066  n4cyclfrgr  28072  occon2  29067  occon3  29076  atexch  30160  sigaclci  31393  fisshasheq  32354  pfxwlk  32372  cusgr3cyclex  32385  frmin  33086  idinside  33547  exrecfnlem  34662  poimirlem32  34926  heibor1lem  35089  axc16g-o  36072  axc11-o  36089  aomclem2  39662  frege124d  40113  tratrb  40877  trsspwALT2  41160  leltletr  43500