MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sps Structured version   Visualization version   GIF version

Theorem sps 2174
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
sps.1 (𝜑𝜓)
Assertion
Ref Expression
sps (∀𝑥𝜑𝜓)

Proof of Theorem sps
StepHypRef Expression
1 sp 2172 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 17 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  2sp  2175  19.2g  2177  nfim1  2190  axc16g  2252  drsb2  2258  axc11r  2379  axc15  2438  axc15OLD  2439  equvel  2474  sb1OLD  2503  sb4a  2505  dfsb1  2506  dfsb2  2528  drsb1  2531  nfsb4t  2535  sbi1OLD  2538  sbco2  2549  sbco3  2551  sb9  2557  sbal1  2568  sbal2  2569  dfsb2ALT  2587  nfsb4tALT  2600  sbi1ALT  2602  sbco2ALT  2611  eujustALT  2653  2eu6  2740  ralcom2  3364  ceqsalgALT  3531  reu6  3716  sbcal  3832  rexdifi  4121  reldisj  4400  dfnfc2  4850  nfnid  5268  eusvnfb  5285  mosubopt  5392  dfid3  5456  fv3  6682  fvmptt  6781  fnoprabg  7264  wfrlem5  7950  pssnn  8725  kmlem16  9580  nd3  10000  axunndlem1  10006  axunnd  10007  axpowndlem1  10008  axregndlem1  10013  axregndlem2  10014  axacndlem5  10022  fundmpss  32907  fprlem1  33035  frrlem15  33040  nalfal  33649  unisym1  33669  bj-sbsb  34058  bj-ax9  34114  wl-nfimf1  34649  wl-dral1d  34653  wl-nfs1t  34659  wl-sb8t  34670  wl-sbhbt  34672  wl-equsb4  34675  wl-sbalnae  34680  wl-2spsbbi  34683  wl-mo3t  34694  wl-ax11-lem5  34703  wl-ax11-lem8  34706  cotrintab  39854  pm11.57  40601  axc5c4c711toc7  40616  axc11next  40618  pm14.122b  40635  dropab1  40659  dropab2  40660  ax6e2eq  40771
  Copyright terms: Public domain W3C validator