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  2520  rspc2vd  3895  trintss  5231  onfununi  8342  smoiun  8362  findcard2  9173  findcard3  9267  inficl  9410  en3lplem2  9607  infxpenlem  10085  alephordi  10146  cardaleph  10161  pwsdompw  10274  cfslb2n  10339  isf32lem10  10433  axdc4lem  10526  zorn2lem2  10568  alephreg  10660  inar1  10853  tskuni  10861  grudomon  10895  nqereu  11007  leltletr  11394  ltleletr  11396  elfz0ubfz0  13759  ssnn0fi  14121  caubnd  15519  sqreulem  15520  bezoutlem1  16705  rppwr  16727  pcprendvds  17011  prmreclem3  17089  ptcmpfi  24125  ufilen  24242  fcfnei  24347  bcthlem5  25642  aaliou  26658  bdayfinbndlem1  28846  wlkres  30242  pfxwlk  30259  wlkiswwlks2  30457  3cyclfrgrrn1  30879  n4cyclfrgr  30885  occon2  31883  occon3  31892  atexch  32976  dfufd2lem  34074  sigaclci  34757  onvfowev  35878  fisshasheq  35882  cusgr3cyclex  35890  idinside  36829  exrecfnlem  38282  poimirlem32  38550  heibor1lem  38723  axc16g-o  39971  axc11-o  39988  aomclem2  44041  frege124d  44746  tratrb  45504  trsspwALT2  45786