Theorem sps 2178

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2sp  2179  19.2g  2181  nfim1  2192  axc16g  2252  drsb2  2258  axc11r  2366  axc15  2422  equvel  2456  sb1OLD  2482  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  eujustALT  2572  2eu6  2658  ralcom2  3290  ceqsalgALT  3465  reu6  3661  sbcal  3780  rexdifi  4080  reldisjOLD  4386  dfnfc2  4863  nfnid  5298  eusvnfb  5316  mosubopt  5424  dfid3  5492  fv3  6792  fvmptt  6895  fnoprabg  7397  fprlem1  8116  wfrlem5OLD  8144  pssnn  8951  pssnnOLD  9040  frrlem15  9515  kmlem16  9921  nd3  10345  axunndlem1  10351  axunnd  10352  axpowndlem1  10353  axregndlem1  10358  axregndlem2  10359  axacndlem5  10367  fundmpss  33740  nalfal  34592  unisym1  34612  bj-sbsb  35020  wl-nfimf1  35685  wl-axc11r  35689  wl-dral1d  35690  wl-nfs1t  35696  wl-sb8t  35707  wl-sbhbt  35709  wl-equsb4  35712  wl-sbalnae  35717  wl-2spsbbi  35720  wl-mo3t  35731  wl-ax11-lem5  35740  wl-ax11-lem8  35743  cotrintab  41222  pm11.57  42007  axc5c4c711toc7  42022  axc11next  42024  pm14.122b  42041  dropab1  42065  dropab2  42066  ax6e2eq  42177