Theorem sps 2192

Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)

Hypothesis

Ref	Expression
sps.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
sps	⊢ (∀𝑥𝜑 → 𝜓)

Proof of Theorem sps

Step	Hyp	Ref	Expression
1		sp 2190	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 17	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  2sp  2193  19.2g  2195  nfim1  2206  axc16g  2267  drsb2  2273  axc11r  2372  axc15  2426  equvel  2460  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2532  sbal2  2533  eujustALT  2572  2eu6  2657  ralcom2  3347  ceqsalgALT  3477  reu6  3684  rexdifi  4102  dfnfc2  4885  nfnid  5320  eusvnfb  5338  mosubopt  5458  dfid3  5522  fv3  6852  fvmptt  6961  fnoprabg  7481  fprlem1  8242  pssnn  9093  frrlem15  9669  kmlem16  10076  nd3  10500  axunndlem1  10506  axunnd  10507  axpowndlem1  10508  axregndlem1  10513  axregndlem2  10514  axacndlem5  10522  axsepg2  35238  axsepg2ALT  35239  axnulg  35264  fundmpss  35961  nalfal  36597  unisym1  36617  bj-sbsb  37038  wl-nfimf1  37727  wl-axc11r  37731  wl-dral1d  37732  wl-nfs1t  37738  wl-sb8t  37753  wl-sbhbt  37755  wl-equsb4  37758  wl-sbalnae  37763  wl-2spsbbi  37766  wl-mo3t  37777  cotrintab  43851  pm11.57  44626  axc5c4c711toc7  44641  axc11next  44643  pm14.122b  44660  dropab1  44683  dropab2  44684  ax6e2eq  44794