Theorem sps 2185

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 2183	. 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 2007  ax-12 2177

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

This theorem is referenced by:  2sp  2186  19.2g  2188  nfim1  2199  axc16g  2260  drsb2  2266  axc11r  2371  axc15  2427  equvel  2461  sb4a  2485  dfsb1  2486  dfsb2  2498  drsb1  2500  nfsb4t  2504  sbco2  2516  sbco3  2518  sb9  2524  sbal1  2533  sbal2  2534  eujustALT  2572  2eu6  2657  ralcom2  3377  ceqsalgALT  3518  reu6  3732  sbcal  3849  rexdifi  4150  dfnfc2  4929  nfnid  5375  eusvnfb  5393  mosubopt  5515  dfid3  5581  fv3  6924  fvmptt  7036  fnoprabg  7556  fprlem1  8325  wfrlem5OLD  8353  pssnn  9208  frrlem15  9797  kmlem16  10206  nd3  10629  axunndlem1  10635  axunnd  10636  axpowndlem1  10637  axregndlem1  10642  axregndlem2  10643  axacndlem5  10651  axsepg2  35096  axsepg2ALT  35097  axnulg  35106  fundmpss  35767  nalfal  36404  unisym1  36424  bj-sbsb  36838  wl-nfimf1  37527  wl-axc11r  37531  wl-dral1d  37532  wl-nfs1t  37538  wl-sb8t  37553  wl-sbhbt  37555  wl-equsb4  37558  wl-sbalnae  37563  wl-2spsbbi  37566  wl-mo3t  37577  wl-ax11-lem5  37590  wl-ax11-lem8  37593  cotrintab  43627  pm11.57  44408  axc5c4c711toc7  44423  axc11next  44425  pm14.122b  44442  dropab1  44466  dropab2  44467  ax6e2eq  44577