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  2493  rspc2vd  3959  trintss  5284  onfununi  8380  smoiun  8400  findcard2  9203  findcard3  9316  findcard3OLD  9317  inficl  9463  en3lplem2  9651  infxpenlem  10051  alephordi  10112  cardaleph  10127  pwsdompw  10241  cfslb2n  10306  isf32lem10  10400  axdc4lem  10493  zorn2lem2  10535  alephreg  10620  inar1  10813  tskuni  10821  grudomon  10855  nqereu  10967  leltletr  11350  ltleletr  11352  elfz0ubfz0  13669  ssnn0fi  14023  caubnd  15394  sqreulem  15395  bezoutlem1  16573  rppwr  16594  pcprendvds  16874  prmreclem3  16952  ptcmpfi  23837  ufilen  23954  fcfnei  24059  bcthlem5  25376  aaliou  26395  wlkres  29703  wlkiswwlks2  29905  3cyclfrgrrn1  30314  n4cyclfrgr  30320  occon2  31317  occon3  31326  atexch  32410  dfufd2lem  33557  sigaclci  34113  fisshasheq  35099  pfxwlk  35108  cusgr3cyclex  35121  idinside  36066  exrecfnlem  37362  poimirlem32  37639  heibor1lem  37796  axc16g-o  38916  axc11-o  38933  aomclem2  43044  frege124d  43751  tratrb  44534  trsspwALT2  44817