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  2488  rspc2vd  3901  trintss  5220  onfununi  8271  smoiun  8291  findcard2  9088  findcard3  9187  findcard3OLD  9188  inficl  9334  en3lplem2  9528  infxpenlem  9926  alephordi  9987  cardaleph  10002  pwsdompw  10116  cfslb2n  10181  isf32lem10  10275  axdc4lem  10368  zorn2lem2  10410  alephreg  10495  inar1  10688  tskuni  10696  grudomon  10730  nqereu  10842  leltletr  11225  ltleletr  11227  elfz0ubfz0  13553  ssnn0fi  13910  caubnd  15284  sqreulem  15285  bezoutlem1  16468  rppwr  16489  pcprendvds  16770  prmreclem3  16848  ptcmpfi  23716  ufilen  23833  fcfnei  23938  bcthlem5  25244  aaliou  26262  wlkres  29632  wlkiswwlks2  29838  3cyclfrgrrn1  30247  n4cyclfrgr  30253  occon2  31250  occon3  31259  atexch  32343  dfufd2lem  33499  sigaclci  34101  fisshasheq  35090  pfxwlk  35099  cusgr3cyclex  35111  idinside  36060  exrecfnlem  37355  poimirlem32  37634  heibor1lem  37791  axc16g-o  38915  axc11-o  38932  aomclem2  43031  frege124d  43737  tratrb  44513  trsspwALT2  44795