MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chvar Structured version   Unicode version

Theorem chvar 1982
Description: Implicit substitution of  y for  x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
chvar.1  |-  F/ x ps
chvar.2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
chvar.3  |-  ph
Assertion
Ref Expression
chvar  |-  ps

Proof of Theorem chvar
StepHypRef Expression
1 chvar.1 . . 3  |-  F/ x ps
2 chvar.2 . . . 4  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
32biimpd 207 . . 3  |-  ( x  =  y  ->  ( ph  ->  ps ) )
41, 3spim 1975 . 2  |-  ( A. x ph  ->  ps )
5 chvar.3 . 2  |-  ph
64, 5mpg 1603 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  chvarv  1983  csbhypf  3454  axrep2  4560  axrep3  4561  opelopabsb  4757  tfindes  6675  findes  6708  dfoprab4f  6839  dom2lem  7552  zfcndrep  8988  pwfseqlem4a  9035  pwfseqlem4  9036  uzind4s  11137  seqof2  12129  gsumcom2  16794  mdetralt2  18878  mdetunilem2  18882  ptcldmpt  19850  elmptrab  20063  isfildlem  20093  dvmptfsum  22111  dvfsumlem2  22163  fmptcof2  27174  measiun  27829  lgamgulmlem2  28212  setinds  28787  wfisg  28866  frinsg  28902  ptrest  29625  fdc1  29842  sbcalf  30120  sbcexf  30121  fphpd  30354  monotuz  30481  monotoddzz  30483  oddcomabszz  30484  setindtrs  30571  flcidc  30728  monoords  31073  fmul01  31130  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climmulf  31146  climexp  31147  climsuse  31150  climrecf  31151  climinff  31153  climaddf  31157  mullimc  31158  limcperiod  31170  neglimc  31189  addlimc  31190  0ellimcdiv  31191  cncfshift  31212  cncfperiod  31217  icccncfext  31226  iblspltprt  31291  itgspltprt  31297  stoweidlem3  31303  stoweidlem34  31334  stoweidlem42  31342  stoweidlem48  31348  dirkercncflem2  31404  fourierdlem15  31422  fourierdlem34  31441  fourierdlem42  31449  fourierdlem48  31455  fourierdlem50  31457  fourierdlem62  31469  fourierdlem73  31480  fourierdlem79  31486  fourierdlem81  31488  fourierdlem92  31499  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  bnj849  33062  bnj1014  33097  bnj1384  33167  bnj1489  33191  bnj1497  33195  fsumshftd  33754  fsumshftdOLD  33755
  Copyright terms: Public domain W3C validator