Theorem sylsyld 58

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 45	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  66  axc16gALT  2354  trint0  4692  onfununi  7303  smoiun  7323  findcard2  8063  findcard3  8066  inficl  8192  en3lplem2  8373  r1sdom  8498  infxpenlem  8697  alephordi  8758  cardaleph  8773  pwsdompw  8887  cfslb2n  8951  isf32lem10  9045  axdc4lem  9138  zorn2lem2  9180  alephreg  9261  inar1  9454  tskuni  9462  grudomon  9496  nqereu  9608  ltleletr  9982  elfz0ubfz0  12270  ssnn0fi  12604  caubnd  13895  sqreulem  13896  bezoutlem1  15043  pcprendvds  15332  prmreclem3  15409  ptcmpfi  21374  ufilen  21492  fcfnei  21597  bcthlem5  22878  aaliou  23842  cusgrarn  25782  3cyclfrgrarn1  26333  n4cyclfrgra  26339  occon2  27365  occon3  27374  atexch  28458  sigaclci  29356  frmin  30817  idinside  31195  poimirlem32  32435  heibor1lem  32602  axc16g-o  33061  axc11-o  33078  aomclem2  36467  frege124d  36896  tratrb  37591  trsspwALT2  37892  leltletr  39765  1wlkres  40901  1wlkiswwlks2  41094  rspc2vd  41459  3cyclfrgrrn1  41477  n4cyclfrgr  41483