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  3899  trintss  5225  onfununi  8283  smoiun  8303  findcard2  9101  findcard3  9195  inficl  9340  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  11236  ltleletr  11238  elfz0ubfz0  13560  ssnn0fi  13920  caubnd  15294  sqreulem  15295  bezoutlem1  16478  rppwr  16499  pcprendvds  16780  prmreclem3  16858  ptcmpfi  23769  ufilen  23886  fcfnei  23991  bcthlem5  25296  aaliou  26314  bdayfinbndlem1  28475  wlkres  29754  wlkiswwlks2  29960  3cyclfrgrrn1  30372  n4cyclfrgr  30378  occon2  31375  occon3  31384  atexch  32468  dfufd2lem  33641  sigaclci  34309  fisshasheq  35328  pfxwlk  35337  cusgr3cyclex  35349  idinside  36297  exrecfnlem  37631  poimirlem32  37900  heibor1lem  38057  axc16g-o  39307  axc11-o  39324  aomclem2  43409  frege124d  44114  tratrb  44889  trsspwALT2  45171