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  2495  rspc2vd  3927  trintss  5253  onfununi  8360  smoiun  8380  findcard2  9183  findcard3  9295  findcard3OLD  9296  inficl  9442  en3lplem2  9632  infxpenlem  10032  alephordi  10093  cardaleph  10108  pwsdompw  10222  cfslb2n  10287  isf32lem10  10381  axdc4lem  10474  zorn2lem2  10516  alephreg  10601  inar1  10794  tskuni  10802  grudomon  10836  nqereu  10948  leltletr  11331  ltleletr  11333  elfz0ubfz0  13654  ssnn0fi  14008  caubnd  15382  sqreulem  15383  bezoutlem1  16563  rppwr  16584  pcprendvds  16865  prmreclem3  16943  ptcmpfi  23756  ufilen  23873  fcfnei  23978  bcthlem5  25285  aaliou  26303  wlkres  29655  wlkiswwlks2  29862  3cyclfrgrrn1  30271  n4cyclfrgr  30277  occon2  31274  occon3  31283  atexch  32367  dfufd2lem  33569  sigaclci  34168  fisshasheq  35142  pfxwlk  35151  cusgr3cyclex  35163  idinside  36107  exrecfnlem  37402  poimirlem32  37681  heibor1lem  37838  axc16g-o  38957  axc11-o  38974  aomclem2  43046  frege124d  43752  tratrb  44528  trsspwALT2  44810