Theorem sps 2190

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

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

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

This theorem is referenced by:  2sp  2191  19.2g  2193  nfim1  2204  axc16g  2265  drsb2  2271  axc11r  2370  axc15  2424  equvel  2458  sb4a  2482  dfsb1  2483  dfsb2  2495  drsb1  2497  nfsb4t  2501  sbco2  2513  sbco3  2515  sb9  2521  sbal1  2530  sbal2  2531  eujustALT  2569  2eu6  2654  ralcom2  3344  ceqsalgALT  3474  reu6  3681  rexdifi  4099  dfnfc2  4880  nfnid  5315  eusvnfb  5333  mosubopt  5453  dfid3  5517  fv3  6846  fvmptt  6955  fnoprabg  7475  fprlem1  8236  pssnn  9085  frrlem15  9657  kmlem16  10064  nd3  10487  axunndlem1  10493  axunnd  10494  axpowndlem1  10495  axregndlem1  10500  axregndlem2  10501  axacndlem5  10509  axsepg2  35115  axsepg2ALT  35116  axnulg  35140  fundmpss  35832  nalfal  36468  unisym1  36488  bj-sbsb  36902  wl-nfimf1  37591  wl-axc11r  37595  wl-dral1d  37596  wl-nfs1t  37602  wl-sb8t  37617  wl-sbhbt  37619  wl-equsb4  37622  wl-sbalnae  37627  wl-2spsbbi  37630  wl-mo3t  37641  cotrintab  43731  pm11.57  44506  axc5c4c711toc7  44521  axc11next  44523  pm14.122b  44540  dropab1  44563  dropab2  44564  ax6e2eq  44674