Theorem sylsyld 59

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 46	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  67  axc16gALT  2355  trint0  4698  onfununi  7325  smoiun  7345  findcard2  8085  findcard3  8088  inficl  8214  en3lplem2  8395  r1sdom  8520  infxpenlem  8719  alephordi  8780  cardaleph  8795  pwsdompw  8909  cfslb2n  8973  isf32lem10  9067  axdc4lem  9160  zorn2lem2  9202  alephreg  9283  inar1  9476  tskuni  9484  grudomon  9518  nqereu  9630  ltleletr  10009  elfz0ubfz0  12312  ssnn0fi  12646  caubnd  13946  sqreulem  13947  bezoutlem1  15094  pcprendvds  15383  prmreclem3  15460  ptcmpfi  21426  ufilen  21544  fcfnei  21649  bcthlem5  22933  aaliou  23897  cusgrarn  25988  3cyclfrgrarn1  26539  n4cyclfrgra  26545  occon2  27531  occon3  27540  atexch  28624  sigaclci  29522  frmin  30983  idinside  31361  poimirlem32  32611  heibor1lem  32778  axc16g-o  33237  axc11-o  33254  aomclem2  36643  frege124d  37072  tratrb  37767  trsspwALT2  38068  leltletr  39940  1wlkres  40879  1wlkiswwlks2  41072  rspc2vd  41437  3cyclfrgrrn1  41455  n4cyclfrgr  41461