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  680  axc16gALT  2494  rspc2vd  3879  trintss  5204  onfununi  8143  smoiun  8163  findcard2  8909  findcard2OLD  8986  findcard3  8987  inficl  9114  en3lplem2  9301  frmin  9438  infxpenlem  9700  alephordi  9761  cardaleph  9776  pwsdompw  9891  cfslb2n  9955  isf32lem10  10049  axdc4lem  10142  zorn2lem2  10184  alephreg  10269  inar1  10462  tskuni  10470  grudomon  10504  nqereu  10616  ltleletr  10998  elfz0ubfz0  13289  ssnn0fi  13633  caubnd  14998  sqreulem  14999  bezoutlem1  16175  rppwr  16197  pcprendvds  16469  prmreclem3  16547  ptcmpfi  22872  ufilen  22989  fcfnei  23094  bcthlem5  24397  aaliou  25403  wlkres  27940  wlkiswwlks2  28141  3cyclfrgrrn1  28550  n4cyclfrgr  28556  occon2  29551  occon3  29560  atexch  30644  sigaclci  32000  fisshasheq  32973  pfxwlk  32985  cusgr3cyclex  32998  idinside  34313  exrecfnlem  35477  poimirlem32  35736  heibor1lem  35894  axc16g-o  36875  axc11-o  36892  aomclem2  40796  frege124d  41258  tratrb  42045  trsspwALT2  42328  leltletr  44673