Theorem sps 2182

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

Syntax hints:   → wi 4  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  2sp  2183  19.2g  2185  nfim1  2197  axc16g  2258  drsb2  2264  axc11r  2375  axc15  2433  equvel  2468  sb1OLD  2496  sb4a  2498  dfsb1  2499  dfsb2  2511  drsb1  2513  nfsb4t  2517  sbi1OLD  2519  sbco2  2530  sbco3  2532  sb9  2538  sbal1  2548  sbal2  2549  dfsb2ALT  2567  nfsb4tALT  2580  sbi1ALT  2582  sbco2ALT  2591  eujustALT  2632  2eu6  2719  ralcom2  3316  ceqsalgALT  3477  reu6  3665  sbcal  3780  rexdifi  4073  reldisjOLD  4360  dfnfc2  4822  nfnid  5241  eusvnfb  5259  mosubopt  5365  dfid3  5427  fv3  6663  fvmptt  6765  fnoprabg  7254  wfrlem5  7942  pssnn  8720  kmlem16  9576  nd3  10000  axunndlem1  10006  axunnd  10007  axpowndlem1  10008  axregndlem1  10013  axregndlem2  10014  axacndlem5  10022  fundmpss  33122  fprlem1  33250  frrlem15  33255  nalfal  33864  unisym1  33884  bj-sbsb  34275  bj-ax9  34340  wl-nfimf1  34931  wl-axc11r  34935  wl-dral1d  34936  wl-nfs1t  34942  wl-sb8t  34953  wl-sbhbt  34955  wl-equsb4  34958  wl-sbalnae  34963  wl-2spsbbi  34966  wl-mo3t  34977  wl-ax11-lem5  34986  wl-ax11-lem8  34989  cotrintab  40314  pm11.57  41093  axc5c4c711toc7  41108  axc11next  41110  pm14.122b  41127  dropab1  41151  dropab2  41152  ax6e2eq  41263