Theorem chvarv 2019

Description: Implicit substitution of y for x into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)

Hypotheses

Ref	Expression
chvarv.1	|- ( x = y -> ( ph <-> ps ) )
chvarv.2	|- ph

Assertion

Ref	Expression
chvarv	|- ps

Distinct variable group:   ps, x

Allowed substitution hints:   ph( x, y)   ps( y)

Proof of Theorem chvarv

Step	Hyp	Ref	Expression
1		nfv 1712	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 2018	1 |- ps

Syntax hints:   -> wi 4   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859  ax-13 2004

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622

This theorem is referenced by:  axext3OLD  2435  axrep1  4551  axsep2  4561  isso2i  4821  tz6.12f  5866  dfac12lem2  8515  wunex2  9105  ltordlem  10074  prodfdiv  13790  iscatd2  15173  yoniso  15756  mrcmndind  16199  gsum2dlem2  17197  gsum2dOLD  17199  isdrngrd  17620  frlmphl  18986  frlmup1  19003  mdetralt  19280  mdetunilem9  19292  neiptoptop  19802  neiptopnei  19803  cnextcn  20736  cnextfres  20737  ustuqtop4  20916  dscmet  21262  nrmmetd  21264  rolle  22560  numclwlk2lem2f1o  25310  chscllem2  26757  esumcvg  28318  eulerpartlemgvv  28582  eulerpartlemn  28587  ftc1anclem7  30339  ftc1anc  30341  fdc  30481  fdc1  30482  iscringd  30639  ismrcd2  30874  fphpdo  30993  monotoddzzfi  31120  monotoddzz  31121  mendlmod  31386  dvgrat  31437  cvgdvgrat  31438  binomcxplemnotnn0  31505  monoords  31738  limcperiod  31876  sumnnodd  31878  cncfshift  31918  cncfperiod  31923  icccncfext  31932  fperdvper  31957  dvnprodlem1  31985  dvnprodlem2  31986  dvnprodlem3  31987  iblspltprt  32014  itgspltprt  32020  stoweidlem43  32067  stoweidlem62  32086  dirkercncflem2  32128  fourierdlem12  32143  fourierdlem15  32146  fourierdlem34  32165  fourierdlem41  32172  fourierdlem42  32173  fourierdlem48  32179  fourierdlem50  32181  fourierdlem51  32182  fourierdlem73  32204  fourierdlem79  32210  fourierdlem81  32212  fourierdlem83  32214  fourierdlem92  32223  fourierdlem94  32225  fourierdlem103  32234  fourierdlem104  32235  fourierdlem111  32242  fourierdlem112  32243  fourierdlem113  32244  etransclem2  32261  etransclem46  32305  bnj1326  34502