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  2529  rspc2vd  3932  trintss  5189  onfununi  7978  smoiun  7998  findcard2  8758  findcard3  8761  inficl  8889  en3lplem2  9076  infxpenlem  9439  alephordi  9500  cardaleph  9515  pwsdompw  9626  cfslb2n  9690  isf32lem10  9784  axdc4lem  9877  zorn2lem2  9919  alephreg  10004  inar1  10197  tskuni  10205  grudomon  10239  nqereu  10351  ltleletr  10733  elfz0ubfz0  13012  ssnn0fi  13354  caubnd  14718  sqreulem  14719  bezoutlem1  15887  pcprendvds  16177  prmreclem3  16254  ptcmpfi  22421  ufilen  22538  fcfnei  22643  bcthlem5  23931  aaliou  24927  wlkres  27452  wlkiswwlks2  27653  3cyclfrgrrn1  28064  n4cyclfrgr  28070  occon2  29065  occon3  29074  atexch  30158  sigaclci  31391  fisshasheq  32352  pfxwlk  32370  cusgr3cyclex  32383  frmin  33084  idinside  33545  exrecfnlem  34663  poimirlem32  34939  heibor1lem  35102  axc16g-o  36085  axc11-o  36102  aomclem2  39675  frege124d  40126  tratrb  40890  trsspwALT2  41173  leltletr  43513