Theorem chvar 2262

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

Step	Hyp	Ref	Expression
1		chvar.1	. . 3 |- F/ x ps
2		chvar.2	. . . 4 |- ( x = y -> ( ph <-> ps ) )
3	2	biimpd 219	. . 3 |- ( x = y -> ( ph -> ps ) )
4	1, 3	spim 2254	. 2 |- ( A. x ph -> ps )
5		chvar.3	. 2 |- ph
6	4, 5	mpg 1724	1 |- ps

Syntax hints:   -> wi 4   <-> wb 196   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  chvarvOLD  2264  csbhypf  3552  axrep2  4773  axrep3  4774  opelopabsb  4985  wfisg  5715  tfindes  7062  findes  7096  dfoprab4f  7226  dom2lem  7995  zfcndrep  9436  pwfseqlem4a  9483  pwfseqlem4  9484  uzind4s  11748  seqof2  12859  fsumsplitf  14472  fproddivf  14718  fprodsplitf  14719  gsumcom2  18374  mdetralt2  20415  mdetunilem2  20419  ptcldmpt  21417  elmptrab  21630  isfildlem  21661  dvmptfsum  23738  dvfsumlem2  23790  lgamgulmlem2  24756  fmptcof2  29457  aciunf1lem  29462  fsumiunle  29575  esum2dlem  30154  fiunelros  30237  measiun  30281  bnj849  30995  bnj1014  31030  bnj1384  31100  bnj1489  31124  bnj1497  31128  setinds  31683  frinsg  31742  finxpreclem6  33233  ptrest  33408  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  fdc1  33542  fsumshftd  34237  fsumshftdOLD  34238  fphpd  37380  monotuz  37506  monotoddzz  37508  oddcomabszz  37509  setindtrs  37592  flcidc  37744  binomcxplemnotnn0  38555  fiiuncl  39234  disjf1  39369  disjinfi  39380  supxrleubrnmptf  39680  fsumclf  39801  fsummulc1f  39802  fsumnncl  39803  fsumf1of  39806  fsumiunss  39807  fsumreclf  39808  fsumlessf  39809  fsumsermpt  39811  fmul01  39812  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fprodexp  39826  fprodabs2  39827  climmulf  39836  climexp  39837  climsuse  39840  climrecf  39841  climinff  39843  climaddf  39847  mullimc  39848  neglimc  39879  addlimc  39880  0ellimcdiv  39881  climsubmpt  39892  climreclf  39896  climeldmeqmpt  39900  climfveqmpt  39903  fnlimfvre  39906  climfveqf  39912  climfveqmpt3  39914  climeldmeqf  39915  climeqf  39920  climeldmeqmpt3  39921  climinf2  39939  climinf2mpt  39946  climinfmpt  39947  limsupequz  39955  limsupequzmptf  39963  fprodcncf  40114  dvmptmulf  40152  dvnmptdivc  40153  dvnmul  40158  dvmptfprod  40160  stoweidlem3  40220  stoweidlem34  40251  stoweidlem42  40259  stoweidlem48  40265  fourierdlem112  40435  sge0lempt  40627  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0ltfirpmpt2  40643  sge0isummpt2  40649  sge0xaddlem2  40651  sge0xadd  40652  meadjiun  40683  voliunsge0lem  40689  meaiininc  40701  hoimbl2  40879  vonhoire  40886  vonn0ioo2  40904  vonn0icc2  40906  salpreimagtlt  40939  smflimlem3  40981