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

Theorem sps 2053
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 2051 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 17 1 (∀𝑥𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  2sp  2054  19.2g  2056  nfim1  2065  axc16g  2130  axc11rvOLD  2136  axc11r  2186  axc15  2302  ax12v2OLD  2341  equvel  2346  dfsb2  2372  drsb1  2376  drsb2  2377  nfsb4t  2388  sbi1  2391  sbco2  2414  sbco3  2416  sb9  2425  sbal1  2459  eujustALT  2472  2eu6  2557  ralcom2  3097  ceqsalgALT  3220  reu6  3381  sbcal  3471  reldisj  3997  dfnfc2  4425  dfnfc2OLD  4426  eusvnfb  4827  nfnid  4862  mosubopt  4937  dfid3  4995  issref  5473  fv3  6168  fvmptt  6261  fnoprabg  6721  wfrlem5  7371  pssnn  8130  kmlem16  8939  nd3  9363  axunndlem1  9369  axunnd  9370  axpowndlem1  9371  axregndlem1  9376  axregndlem2  9377  axacndlem5  9385  fundmpss  31403  frrlem5  31520  nalf  32079  unisym1  32099  bj-sbsb  32502  bj-mo3OLD  32512  bj-ax9  32572  bj-xnex  32736  wl-nfimf1  32980  wl-dral1d  32985  wl-nfs1t  32991  wl-sb8t  33000  wl-sbhbt  33002  wl-equsb4  33005  wl-sbalnae  33012  wl-mo3t  33025  wl-ax11-lem5  33033  wl-ax11-lem8  33036  wl-sbcom3  33039  cotrintab  37437  pm11.57  38106  axc5c4c711toc7  38122  axc11next  38124  pm14.122b  38141  dropab1  38168  dropab2  38169  ax6e2eq  38290
  Copyright terms: Public domain W3C validator