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  2370  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  2571  2eu6  2656  ralcom2  3356  ceqsalgALT  3497  reu6  3709  sbcal  3825  rexdifi  4125  dfnfc2  4905  nfnid  5345  eusvnfb  5363  mosubopt  5485  dfid3  5551  fv3  6894  fvmptt  7006  fnoprabg  7530  fprlem1  8299  wfrlem5OLD  8327  pssnn  9182  frrlem15  9771  kmlem16  10180  nd3  10603  axunndlem1  10609  axunnd  10610  axpowndlem1  10611  axregndlem1  10616  axregndlem2  10617  axacndlem5  10625  axsepg2  35113  axsepg2ALT  35114  axnulg  35123  fundmpss  35784  nalfal  36421  unisym1  36441  bj-sbsb  36855  wl-nfimf1  37544  wl-axc11r  37548  wl-dral1d  37549  wl-nfs1t  37555  wl-sb8t  37570  wl-sbhbt  37572  wl-equsb4  37575  wl-sbalnae  37580  wl-2spsbbi  37583  wl-mo3t  37594  wl-ax11-lem5  37607  wl-ax11-lem8  37610  cotrintab  43638  pm11.57  44413  axc5c4c711toc7  44428  axc11next  44430  pm14.122b  44447  dropab1  44471  dropab2  44472  ax6e2eq  44582