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  684  axc16gALT  2492  rspc2vd  3894  trintss  5220  onfununi  8270  smoiun  8290  findcard2  9085  findcard3  9178  inficl  9320  en3lplem2  9514  infxpenlem  9915  alephordi  9976  cardaleph  9991  pwsdompw  10105  cfslb2n  10170  isf32lem10  10264  axdc4lem  10357  zorn2lem2  10399  alephreg  10484  inar1  10677  tskuni  10685  grudomon  10719  nqereu  10831  leltletr  11215  ltleletr  11217  elfz0ubfz0  13539  ssnn0fi  13899  caubnd  15273  sqreulem  15274  bezoutlem1  16457  rppwr  16478  pcprendvds  16759  prmreclem3  16837  ptcmpfi  23748  ufilen  23865  fcfnei  23970  bcthlem5  25275  aaliou  26293  wlkres  29668  wlkiswwlks2  29874  3cyclfrgrrn1  30286  n4cyclfrgr  30292  occon2  31289  occon3  31298  atexch  32382  dfufd2lem  33558  sigaclci  34217  fisshasheq  35231  pfxwlk  35240  cusgr3cyclex  35252  idinside  36200  exrecfnlem  37496  poimirlem32  37765  heibor1lem  37922  axc16g-o  39106  axc11-o  39123  aomclem2  43212  frege124d  43918  tratrb  44693  trsspwALT2  44975