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  2395  trintss  4802  onfununi  7483  smoiun  7503  findcard2  8241  findcard3  8244  inficl  8372  en3lplem2  8550  r1sdom  8675  infxpenlem  8874  alephordi  8935  cardaleph  8950  pwsdompw  9064  cfslb2n  9128  isf32lem10  9222  axdc4lem  9315  zorn2lem2  9357  alephreg  9442  inar1  9635  tskuni  9643  grudomon  9677  nqereu  9789  ltleletr  10168  elfz0ubfz0  12482  ssnn0fi  12824  caubnd  14142  sqreulem  14143  bezoutlem1  15303  pcprendvds  15592  prmreclem3  15669  ptcmpfi  21664  ufilen  21781  fcfnei  21886  bcthlem5  23171  aaliou  24138  wlkres  26623  wlkiswwlks2  26829  rspc2vd  27245  3cyclfrgrrn1  27265  n4cyclfrgr  27271  occon2  28275  occon3  28284  atexch  29368  sigaclci  30323  frmin  31867  idinside  32316  poimirlem32  33571  heibor1lem  33738  axc16g-o  34538  axc11-o  34555  aomclem2  37942  frege124d  38370  tratrb  39063  trsspwALT2  39363  leltletr  41633