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  2488  rspc2vd  3907  trintss  5228  onfununi  8287  smoiun  8307  findcard2  9105  findcard3  9205  findcard3OLD  9206  inficl  9352  en3lplem2  9542  infxpenlem  9942  alephordi  10003  cardaleph  10018  pwsdompw  10132  cfslb2n  10197  isf32lem10  10291  axdc4lem  10384  zorn2lem2  10426  alephreg  10511  inar1  10704  tskuni  10712  grudomon  10746  nqereu  10858  leltletr  11241  ltleletr  11243  elfz0ubfz0  13569  ssnn0fi  13926  caubnd  15301  sqreulem  15302  bezoutlem1  16485  rppwr  16506  pcprendvds  16787  prmreclem3  16865  ptcmpfi  23676  ufilen  23793  fcfnei  23898  bcthlem5  25204  aaliou  26222  wlkres  29572  wlkiswwlks2  29778  3cyclfrgrrn1  30187  n4cyclfrgr  30193  occon2  31190  occon3  31199  atexch  32283  dfufd2lem  33493  sigaclci  34095  fisshasheq  35075  pfxwlk  35084  cusgr3cyclex  35096  idinside  36045  exrecfnlem  37340  poimirlem32  37619  heibor1lem  37776  axc16g-o  38900  axc11-o  38917  aomclem2  43017  frege124d  43723  tratrb  44499  trsspwALT2  44781