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  685  axc16gALT  2495  rspc2vd  3886  trintss  5211  onfununi  8274  smoiun  8294  findcard2  9092  findcard3  9186  inficl  9331  en3lplem2  9525  infxpenlem  9926  alephordi  9987  cardaleph  10002  pwsdompw  10116  cfslb2n  10181  isf32lem10  10275  axdc4lem  10368  zorn2lem2  10410  alephreg  10496  inar1  10689  tskuni  10697  grudomon  10731  nqereu  10843  leltletr  11228  ltleletr  11230  elfz0ubfz0  13577  ssnn0fi  13938  caubnd  15312  sqreulem  15313  bezoutlem1  16499  rppwr  16520  pcprendvds  16802  prmreclem3  16880  ptcmpfi  23788  ufilen  23905  fcfnei  24010  bcthlem5  25305  aaliou  26315  bdayfinbndlem1  28473  wlkres  29752  wlkiswwlks2  29958  3cyclfrgrrn1  30370  n4cyclfrgr  30376  occon2  31374  occon3  31383  atexch  32467  dfufd2lem  33624  sigaclci  34292  fisshasheq  35313  pfxwlk  35322  cusgr3cyclex  35334  idinside  36282  exrecfnlem  37709  poimirlem32  37987  heibor1lem  38144  axc16g-o  39394  axc11-o  39411  aomclem2  43501  frege124d  44206  tratrb  44981  trsspwALT2  45263