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  axc16gALT  2367  trintss  4769  onfununi  7438  smoiun  7458  findcard2  8200  findcard3  8203  inficl  8331  en3lplem2  8512  r1sdom  8637  infxpenlem  8836  alephordi  8897  cardaleph  8912  pwsdompw  9026  cfslb2n  9090  isf32lem10  9184  axdc4lem  9277  zorn2lem2  9319  alephreg  9404  inar1  9597  tskuni  9605  grudomon  9639  nqereu  9751  ltleletr  10130  elfz0ubfz0  12443  ssnn0fi  12784  caubnd  14098  sqreulem  14099  bezoutlem1  15256  pcprendvds  15545  prmreclem3  15622  ptcmpfi  21616  ufilen  21734  fcfnei  21839  bcthlem5  23125  aaliou  24093  wlkres  26567  wlkiswwlks2  26761  rspc2vd  27129  3cyclfrgrrn1  27149  n4cyclfrgr  27155  occon2  28147  occon3  28156  atexch  29240  sigaclci  30195  frmin  31739  idinside  32191  poimirlem32  33441  heibor1lem  33608  axc16g-o  34219  axc11-o  34236  aomclem2  37625  frege124d  38053  tratrb  38746  trsspwALT2  39046  leltletr  41308