Theorem sps 2219

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

Syntax hints:   → wi 4  ∀wal 1557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  2sp  2220  19.2g  2222  nfim1  2233  axc16g  2294  drsb2  2300  axc11r  2398  axc15  2452  equvel  2486  sb4a  2510  dfsb1  2511  dfsb2  2523  drsb1  2525  nfsb4t  2529  sbco2  2541  sbco3  2543  sb9  2549  sbal1  2558  sbal2  2559  eujustALT  2598  2eu6  2682  ralcom2  3363  ceqsalgALT  3489  reu6  3688  rexdifi  4103  dfnfc2  4886  nfnid  5331  eusvnfb  5349  mosubopt  5478  dfid3  5543  fv3  6881  fvmptt  6992  fnoprabg  7515  fprlem1  8276  pssnn  9133  frrlem15  9712  kmlem16  10119  nd3  10544  axunndlem1  10550  axunnd  10551  axpowndlem1  10552  axregndlem1  10557  axregndlem2  10558  axacndlem5  10566  axsepg3  35401  axsepg3ALT  35402  axsepg5  35404  axnulg  35405  fundmpss  36081  nalfal  36727  unisym1  36747  axtcond  36802  bj-sbsb  37286  wl-nfimf1  37993  wl-axc11r  37997  wl-dral1d  37998  wl-nfs1t  38004  wl-sb8t  38019  wl-sbhbt  38021  wl-equsb4  38024  wl-sbalnae  38029  wl-2spsbbi  38032  wl-mo3t  38043  cotrintab  44154  pm11.57  44929  axc5c4c711toc7  44944  axc11next  44946  pm14.122b  44963  dropab1  44986  dropab2  44987  ax6e2eq  45097  quantgodelALT  47413