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  3947  trintss  5278  onfununi  8381  smoiun  8401  findcard2  9204  findcard3  9318  findcard3OLD  9319  inficl  9465  en3lplem2  9653  infxpenlem  10053  alephordi  10114  cardaleph  10129  pwsdompw  10243  cfslb2n  10308  isf32lem10  10402  axdc4lem  10495  zorn2lem2  10537  alephreg  10622  inar1  10815  tskuni  10823  grudomon  10857  nqereu  10969  leltletr  11352  ltleletr  11354  elfz0ubfz0  13672  ssnn0fi  14026  caubnd  15397  sqreulem  15398  bezoutlem1  16576  rppwr  16597  pcprendvds  16878  prmreclem3  16956  ptcmpfi  23821  ufilen  23938  fcfnei  24043  bcthlem5  25362  aaliou  26380  wlkres  29688  wlkiswwlks2  29895  3cyclfrgrrn1  30304  n4cyclfrgr  30310  occon2  31307  occon3  31316  atexch  32400  dfufd2lem  33577  sigaclci  34133  fisshasheq  35120  pfxwlk  35129  cusgr3cyclex  35141  idinside  36085  exrecfnlem  37380  poimirlem32  37659  heibor1lem  37816  axc16g-o  38935  axc11-o  38952  aomclem2  43067  frege124d  43774  tratrb  44556  trsspwALT2  44839