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  683  axc16gALT  2498  rspc2vd  3972  trintss  5302  onfununi  8397  smoiun  8417  findcard2  9230  findcard3  9346  findcard3OLD  9347  inficl  9494  en3lplem2  9682  infxpenlem  10082  alephordi  10143  cardaleph  10158  pwsdompw  10272  cfslb2n  10337  isf32lem10  10431  axdc4lem  10524  zorn2lem2  10566  alephreg  10651  inar1  10844  tskuni  10852  grudomon  10886  nqereu  10998  leltletr  11381  ltleletr  11383  elfz0ubfz0  13689  ssnn0fi  14036  caubnd  15407  sqreulem  15408  bezoutlem1  16586  rppwr  16607  pcprendvds  16887  prmreclem3  16965  ptcmpfi  23842  ufilen  23959  fcfnei  24064  bcthlem5  25381  aaliou  26398  wlkres  29706  wlkiswwlks2  29908  3cyclfrgrrn1  30317  n4cyclfrgr  30323  occon2  31320  occon3  31329  atexch  32413  dfufd2lem  33542  sigaclci  34096  fisshasheq  35082  pfxwlk  35091  cusgr3cyclex  35104  idinside  36048  exrecfnlem  37345  poimirlem32  37612  heibor1lem  37769  axc16g-o  38890  axc11-o  38907  aomclem2  43012  frege124d  43723  tratrb  44507  trsspwALT2  44790