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  680  axc16gALT  2483  trintss  5080  onfununi  7830  smoiun  7850  findcard2  8604  findcard3  8607  inficl  8735  en3lplem2  8922  infxpenlem  9285  alephordi  9346  cardaleph  9361  pwsdompw  9472  cfslb2n  9536  isf32lem10  9630  axdc4lem  9723  zorn2lem2  9765  alephreg  9850  inar1  10043  tskuni  10051  grudomon  10085  nqereu  10197  ltleletr  10580  elfz0ubfz0  12861  ssnn0fi  13203  caubnd  14552  sqreulem  14553  bezoutlem1  15716  pcprendvds  16006  prmreclem3  16083  ptcmpfi  22105  ufilen  22222  fcfnei  22327  bcthlem5  23614  aaliou  24610  wlkres  27135  wlkresOLD  27137  wlkiswwlks2  27340  rspc2vd  27736  3cyclfrgrrn1  27756  n4cyclfrgr  27762  occon2  28756  occon3  28765  atexch  29849  sigaclci  31008  fisshasheq  31966  cusgr3cyclex  31991  frmin  32693  idinside  33154  exrecfnlem  34191  poimirlem32  34455  heibor1lem  34619  axc16g-o  35601  axc11-o  35618  aomclem2  39140  frege124d  39591  tratrb  40409  trsspwALT2  40692  leltletr  43009