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  682  axc16gALT  2489  rspc2vd  3943  trintss  5283  onfununi  8337  smoiun  8357  findcard2  9160  findcard2OLD  9280  findcard3  9281  findcard3OLD  9282  inficl  9416  en3lplem2  9604  infxpenlem  10004  alephordi  10065  cardaleph  10080  pwsdompw  10195  cfslb2n  10259  isf32lem10  10353  axdc4lem  10446  zorn2lem2  10488  alephreg  10573  inar1  10766  tskuni  10774  grudomon  10808  nqereu  10920  leltletr  11301  ltleletr  11303  elfz0ubfz0  13601  ssnn0fi  13946  caubnd  15301  sqreulem  15302  bezoutlem1  16477  rppwr  16497  pcprendvds  16769  prmreclem3  16847  ptcmpfi  23308  ufilen  23425  fcfnei  23530  bcthlem5  24836  aaliou  25842  wlkres  28916  wlkiswwlks2  29118  3cyclfrgrrn1  29527  n4cyclfrgr  29533  occon2  30528  occon3  30537  atexch  31621  sigaclci  33118  fisshasheq  34092  pfxwlk  34102  cusgr3cyclex  34115  idinside  35044  exrecfnlem  36248  poimirlem32  36508  heibor1lem  36665  axc16g-o  37792  axc11-o  37809  aomclem2  41782  frege124d  42497  tratrb  43282  trsspwALT2  43565