Theorem sps 2197

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 2195	. 2 ⊢ (∀𝑥𝜑 → 𝜑)
2		sps.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	syl 17	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  2sp  2198  19.2g  2200  nfim1  2211  axc16g  2272  drsb2  2278  axc11r  2376  axc15  2430  equvel  2464  sb4a  2488  dfsb1  2489  dfsb2  2501  drsb1  2503  nfsb4t  2507  sbco2  2519  sbco3  2521  sb9  2527  sbal1  2536  sbal2  2537  eujustALT  2576  2eu6  2661  ralcom2  3342  ceqsalgALT  3469  reu6  3674  rexdifi  4087  dfnfc2  4867  nfnid  5311  eusvnfb  5329  mosubopt  5458  dfid3  5523  fv3  6852  fvmptt  6963  fnoprabg  7486  fprlem1  8247  pssnn  9100  frrlem15  9679  kmlem16  10086  nd3  10510  axunndlem1  10516  axunnd  10517  axpowndlem1  10518  axregndlem1  10523  axregndlem2  10524  axacndlem5  10532  axsepg3  35329  axsepg3ALT  35330  axsepg5  35332  axnulg  35333  fundmpss  36002  nalfal  36638  unisym1  36658  axtcond  36713  bj-sbsb  37197  wl-nfimf1  37904  wl-axc11r  37908  wl-dral1d  37909  wl-nfs1t  37915  wl-sb8t  37930  wl-sbhbt  37932  wl-equsb4  37935  wl-sbalnae  37940  wl-2spsbbi  37943  wl-mo3t  37954  cotrintab  44065  pm11.57  44840  axc5c4c711toc7  44855  axc11next  44857  pm14.122b  44874  dropab1  44897  dropab2  44898  ax6e2eq  45008  quantgodelALT  47325