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  681  axc16gALT  2494  rspc2vd  3883  trintss  5208  onfununi  8172  smoiun  8192  findcard2  8947  findcard2OLD  9056  findcard3  9057  inficl  9184  en3lplem2  9371  infxpenlem  9769  alephordi  9830  cardaleph  9845  pwsdompw  9960  cfslb2n  10024  isf32lem10  10118  axdc4lem  10211  zorn2lem2  10253  alephreg  10338  inar1  10531  tskuni  10539  grudomon  10573  nqereu  10685  leltletr  11066  ltleletr  11068  elfz0ubfz0  13360  ssnn0fi  13705  caubnd  15070  sqreulem  15071  bezoutlem1  16247  rppwr  16269  pcprendvds  16541  prmreclem3  16619  ptcmpfi  22964  ufilen  23081  fcfnei  23186  bcthlem5  24492  aaliou  25498  wlkres  28038  wlkiswwlks2  28240  3cyclfrgrrn1  28649  n4cyclfrgr  28655  occon2  29650  occon3  29659  atexch  30743  sigaclci  32100  fisshasheq  33073  pfxwlk  33085  cusgr3cyclex  33098  idinside  34386  exrecfnlem  35550  poimirlem32  35809  heibor1lem  35967  axc16g-o  36948  axc11-o  36965  aomclem2  40880  frege124d  41369  tratrb  42156  trsspwALT2  42439