Theorem sylsyld 62

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 18	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	1, 4	syld 48	1 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpsylsyld  70  syl6an  697  axc16gALT  2524  rspc2vd  3902  trintss  5239  onfununi  8330  smoiun  8350  findcard2  9152  findcard3  9246  inficl  9388  en3lplem2  9585  infxpenlem  10009  alephordi  10070  cardaleph  10085  pwsdompw  10198  cfslb2n  10263  isf32lem10  10357  axdc4lem  10450  zorn2lem2  10492  alephreg  10578  inar1  10771  tskuni  10779  grudomon  10813  nqereu  10925  leltletr  11312  ltleletr  11314  elfz0ubfz0  13672  ssnn0fi  14034  caubnd  15429  sqreulem  15430  bezoutlem1  16614  rppwr  16635  pcprendvds  16917  prmreclem3  16995  ptcmpfi  23999  ufilen  24116  fcfnei  24221  bcthlem5  25516  aaliou  26530  bdayfinbndlem1  28689  wlkres  30047  wlkiswwlks2  30253  3cyclfrgrrn1  30665  n4cyclfrgr  30671  occon2  31669  occon3  31678  atexch  32762  dfufd2lem  33862  sigaclci  34545  onvfowev  35616  fisshasheq  35621  pfxwlk  35629  cusgr3cyclex  35641  idinside  36589  exrecfnlem  38058  poimirlem32  38336  heibor1lem  38493  axc16g-o  39741  axc11-o  39758  aomclem2  43815  frege124d  44520  tratrb  45278  trsspwALT2  45560