Theorem sps 2186

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

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

This theorem is referenced by:  2sp  2187  19.2g  2189  nfim1  2200  axc16g  2261  drsb2  2267  axc11r  2366  axc15  2420  equvel  2454  sb4a  2478  dfsb1  2479  dfsb2  2491  drsb1  2493  nfsb4t  2497  sbco2  2509  sbco3  2511  sb9  2517  sbal1  2526  sbal2  2527  eujustALT  2565  2eu6  2650  ralcom2  3342  ceqsalgALT  3475  reu6  3688  rexdifi  4103  dfnfc2  4883  nfnid  5317  eusvnfb  5335  mosubopt  5457  dfid3  5521  fv3  6844  fvmptt  6954  fnoprabg  7476  fprlem1  8240  pssnn  9092  frrlem15  9672  kmlem16  10079  nd3  10502  axunndlem1  10508  axunnd  10509  axpowndlem1  10510  axregndlem1  10515  axregndlem2  10516  axacndlem5  10524  axsepg2  35048  axsepg2ALT  35049  axnulg  35058  fundmpss  35739  nalfal  36376  unisym1  36396  bj-sbsb  36810  wl-nfimf1  37499  wl-axc11r  37503  wl-dral1d  37504  wl-nfs1t  37510  wl-sb8t  37525  wl-sbhbt  37527  wl-equsb4  37530  wl-sbalnae  37535  wl-2spsbbi  37538  wl-mo3t  37549  wl-ax11-lem5  37562  wl-ax11-lem8  37565  cotrintab  43587  pm11.57  44362  axc5c4c711toc7  44377  axc11next  44379  pm14.122b  44396  dropab1  44420  dropab2  44421  ax6e2eq  44531