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  2494  rspc2vd  3885  trintss  5211  onfununi  8281  smoiun  8301  findcard2  9099  findcard3  9193  inficl  9338  en3lplem2  9534  infxpenlem  9935  alephordi  9996  cardaleph  10011  pwsdompw  10125  cfslb2n  10190  isf32lem10  10284  axdc4lem  10377  zorn2lem2  10419  alephreg  10505  inar1  10698  tskuni  10706  grudomon  10740  nqereu  10852  leltletr  11237  ltleletr  11239  elfz0ubfz0  13586  ssnn0fi  13947  caubnd  15321  sqreulem  15322  bezoutlem1  16508  rppwr  16529  pcprendvds  16811  prmreclem3  16889  ptcmpfi  23778  ufilen  23895  fcfnei  24000  bcthlem5  25295  aaliou  26304  bdayfinbndlem1  28459  wlkres  29737  wlkiswwlks2  29943  3cyclfrgrrn1  30355  n4cyclfrgr  30361  occon2  31359  occon3  31368  atexch  32452  dfufd2lem  33609  sigaclci  34276  fisshasheq  35297  pfxwlk  35306  cusgr3cyclex  35318  idinside  36266  exrecfnlem  37695  poimirlem32  37973  heibor1lem  38130  axc16g-o  39380  axc11-o  39397  aomclem2  43483  frege124d  44188  tratrb  44963  trsspwALT2  45245