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  684  axc16gALT  2494  rspc2vd  3897  trintss  5223  onfununi  8273  smoiun  8293  findcard2  9089  findcard3  9183  inficl  9328  en3lplem2  9522  infxpenlem  9923  alephordi  9984  cardaleph  9999  pwsdompw  10113  cfslb2n  10178  isf32lem10  10272  axdc4lem  10365  zorn2lem2  10407  alephreg  10493  inar1  10686  tskuni  10694  grudomon  10728  nqereu  10840  leltletr  11224  ltleletr  11226  elfz0ubfz0  13548  ssnn0fi  13908  caubnd  15282  sqreulem  15283  bezoutlem1  16466  rppwr  16487  pcprendvds  16768  prmreclem3  16846  ptcmpfi  23757  ufilen  23874  fcfnei  23979  bcthlem5  25284  aaliou  26302  bdayfinbndlem1  28463  wlkres  29742  wlkiswwlks2  29948  3cyclfrgrrn1  30360  n4cyclfrgr  30366  occon2  31363  occon3  31372  atexch  32456  dfufd2lem  33630  sigaclci  34289  fisshasheq  35309  pfxwlk  35318  cusgr3cyclex  35330  idinside  36278  exrecfnlem  37584  poimirlem32  37853  heibor1lem  38010  axc16g-o  39194  axc11-o  39211  aomclem2  43297  frege124d  44002  tratrb  44777  trsspwALT2  45059