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

Theorem sps 2176
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 2174 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 17 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169
This theorem depends on definitions:  df-bi 209  df-ex 1774
This theorem is referenced by:  2sp  2177  19.2g  2179  nfim1  2191  axc16g  2253  drsb2  2259  axc11r  2379  axc15  2437  equvel  2472  sb1OLD  2501  sb4a  2503  dfsb1  2504  dfsb2  2526  drsb1  2529  nfsb4t  2533  sbi1OLD  2536  sbco2  2547  sbco3  2549  sb9  2555  sbal1  2566  sbal2  2567  dfsb2ALT  2585  nfsb4tALT  2598  sbi1ALT  2600  sbco2ALT  2609  eujustALT  2651  2eu6  2738  ralcom2  3362  ceqsalgALT  3529  reu6  3715  sbcal  3831  rexdifi  4120  reldisj  4400  dfnfc2  4848  nfnid  5267  eusvnfb  5284  mosubopt  5391  dfid3  5455  fv3  6681  fvmptt  6781  fnoprabg  7267  wfrlem5  7951  pssnn  8728  kmlem16  9583  nd3  10003  axunndlem1  10009  axunnd  10010  axpowndlem1  10011  axregndlem1  10016  axregndlem2  10017  axacndlem5  10025  fundmpss  32997  fprlem1  33125  frrlem15  33130  nalfal  33739  unisym1  33759  bj-sbsb  34148  bj-ax9  34204  wl-nfimf1  34748  wl-axc11r  34752  wl-dral1d  34753  wl-nfs1t  34759  wl-sb8t  34770  wl-sbhbt  34772  wl-equsb4  34775  wl-sbalnae  34780  wl-2spsbbi  34783  wl-mo3t  34794  wl-ax11-lem5  34803  wl-ax11-lem8  34806  cotrintab  39954  pm11.57  40701  axc5c4c711toc7  40716  axc11next  40718  pm14.122b  40735  dropab1  40759  dropab2  40760  ax6e2eq  40871
  Copyright terms: Public domain W3C validator