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  3910  trintss  5233  onfununi  8310  smoiun  8330  findcard2  9128  findcard3  9229  findcard3OLD  9230  inficl  9376  en3lplem2  9566  infxpenlem  9966  alephordi  10027  cardaleph  10042  pwsdompw  10156  cfslb2n  10221  isf32lem10  10315  axdc4lem  10408  zorn2lem2  10450  alephreg  10535  inar1  10728  tskuni  10736  grudomon  10770  nqereu  10882  leltletr  11265  ltleletr  11267  elfz0ubfz0  13593  ssnn0fi  13950  caubnd  15325  sqreulem  15326  bezoutlem1  16509  rppwr  16530  pcprendvds  16811  prmreclem3  16889  ptcmpfi  23700  ufilen  23817  fcfnei  23922  bcthlem5  25228  aaliou  26246  wlkres  29598  wlkiswwlks2  29805  3cyclfrgrrn1  30214  n4cyclfrgr  30220  occon2  31217  occon3  31226  atexch  32310  dfufd2lem  33520  sigaclci  34122  fisshasheq  35102  pfxwlk  35111  cusgr3cyclex  35123  idinside  36072  exrecfnlem  37367  poimirlem32  37646  heibor1lem  37803  axc16g-o  38927  axc11-o  38944  aomclem2  43044  frege124d  43750  tratrb  44526  trsspwALT2  44808