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 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpsylsyld  70  syl6an  697  axc16gALT  2520  rspc2vd  3895  trintss  5231  onfununi  8349  smoiun  8369  findcard2  9180  findcard3  9274  inficl  9417  en3lplem2  9614  infxpenlem  10092  alephordi  10153  cardaleph  10168  pwsdompw  10281  cfslb2n  10346  isf32lem10  10440  axdc4lem  10533  zorn2lem2  10575  alephreg  10667  inar1  10860  tskuni  10868  grudomon  10902  nqereu  11014  leltletr  11401  ltleletr  11403  elfz0ubfz0  13766  ssnn0fi  14128  caubnd  15526  sqreulem  15527  bezoutlem1  16712  rppwr  16734  pcprendvds  17018  prmreclem3  17096  ptcmpfi  24132  ufilen  24249  fcfnei  24354  bcthlem5  25649  aaliou  26665  bdayfinbndlem1  28853  wlkres  30249  pfxwlk  30266  wlkiswwlks2  30464  3cyclfrgrrn1  30886  n4cyclfrgr  30892  occon2  31890  occon3  31899  atexch  32983  dfufd2lem  34081  sigaclci  34764  onvfowev  35899  fisshasheq  35903  cusgr3cyclex  35911  idinside  36849  exrecfnlem  38303  poimirlem32  38571  heibor1lem  38744  axc16g-o  39992  axc11-o  40009  aomclem2  44057  frege124d  44761  tratrb  45519  trsspwALT2  45801