Theorem sylsyld 62

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 18	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	1, 4	syld 48	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  70  syl6an  696  axc16gALT  2522  rspc2vd  3902  trintss  5238  onfununi  8329  smoiun  8349  findcard2  9150  findcard3  9244  inficl  9386  en3lplem2  9583  infxpenlem  9998  alephordi  10059  cardaleph  10074  pwsdompw  10187  cfslb2n  10253  isf32lem10  10347  axdc4lem  10440  zorn2lem2  10482  alephreg  10568  inar1  10761  tskuni  10769  grudomon  10803  nqereu  10915  leltletr  11302  ltleletr  11304  elfz0ubfz0  13662  ssnn0fi  14023  caubnd  15412  sqreulem  15413  bezoutlem1  16598  rppwr  16619  pcprendvds  16901  prmreclem3  16979  ptcmpfi  23951  ufilen  24068  fcfnei  24173  bcthlem5  25468  aaliou  26482  bdayfinbndlem1  28641  wlkres  29999  wlkiswwlks2  30205  3cyclfrgrrn1  30617  n4cyclfrgr  30623  occon2  31621  occon3  31630  atexch  32714  dfufd2lem  33820  sigaclci  34503  onvfowev  35581  fisshasheq  35587  pfxwlk  35597  cusgr3cyclex  35609  idinside  36557  exrecfnlem  38006  poimirlem32  38284  heibor1lem  38441  axc16g-o  39689  axc11-o  39706  aomclem2  43765  frege124d  44470  tratrb  45228  trsspwALT2  45510