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

Theorem sps 2185
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 2183 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 17 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-12 2178
This theorem depends on definitions:  df-bi 210  df-ex 1787
This theorem is referenced by:  2sp  2186  19.2g  2188  nfim1  2200  axc16g  2260  drsb2  2266  axc11r  2367  axc15  2421  equvel  2455  sb1OLD  2482  sb4a  2484  dfsb1  2485  dfsb2  2497  drsb1  2499  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  eujustALT  2573  2eu6  2659  ralcom2  3265  ceqsalgALT  3430  reu6  3623  sbcal  3740  rexdifi  4034  reldisjOLD  4339  dfnfc2  4817  nfnid  5239  eusvnfb  5257  mosubopt  5364  dfid3  5427  fv3  6686  fvmptt  6789  fnoprabg  7283  wfrlem5  7981  pssnn  8760  pssnnOLD  8808  kmlem16  9658  nd3  10082  axunndlem1  10088  axunnd  10089  axpowndlem1  10090  axregndlem1  10095  axregndlem2  10096  axacndlem5  10104  fundmpss  33304  fprlem1  33447  frrlem15  33452  nalfal  34222  unisym1  34242  bj-sbsb  34640  wl-nfimf1  35297  wl-axc11r  35301  wl-dral1d  35302  wl-nfs1t  35308  wl-sb8t  35319  wl-sbhbt  35321  wl-equsb4  35324  wl-sbalnae  35329  wl-2spsbbi  35332  wl-mo3t  35343  wl-ax11-lem5  35352  wl-ax11-lem8  35355  cotrintab  40751  pm11.57  41529  axc5c4c711toc7  41544  axc11next  41546  pm14.122b  41563  dropab1  41587  dropab2  41588  ax6e2eq  41699
  Copyright terms: Public domain W3C validator