Theorem chvarv 2000

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 1694	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 1999	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 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-13 1985

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604

This theorem is referenced by:  axext3OLD  2424  axrep1  4549  axsep2  4559  isso2i  4822  tz6.12f  5874  dfac12lem2  8527  wunex2  9119  ltordlem  10085  prodfdiv  13687  iscatd2  15060  yoniso  15533  mrcmndind  15976  gsum2dlem2  16977  gsum2dOLD  16979  isdrngrd  17401  frlmphl  18790  frlmup1  18810  mdetralt  19088  mdetunilem9  19100  neiptoptop  19610  neiptopnei  19611  cnextcn  20545  cnextfres  20546  ustuqtop4  20725  dscmet  21071  nrmmetd  21073  rolle  22369  numclwlk2lem2f1o  25083  chscllem2  26534  esumcvg  28070  eulerpartlemgvv  28293  eulerpartlemn  28298  ftc1anclem7  30072  ftc1anc  30074  fdc  30214  fdc1  30215  iscringd  30372  ismrcd2  30607  fphpdo  30727  monotoddzzfi  30854  monotoddzz  30855  mendlmod  31118  dvgrat  31169  cvgdvgrat  31170  monoords  31450  limcperiod  31588  sumnnodd  31590  cncfshift  31630  cncfperiod  31635  icccncfext  31644  fperdvper  31669  dvnprodlem1  31697  dvnprodlem2  31698  dvnprodlem3  31699  iblspltprt  31726  itgspltprt  31732  stoweidlem43  31779  stoweidlem62  31798  dirkercncflem2  31840  fourierdlem12  31855  fourierdlem15  31858  fourierdlem34  31877  fourierdlem41  31884  fourierdlem42  31885  fourierdlem48  31891  fourierdlem50  31893  fourierdlem51  31894  fourierdlem73  31916  fourierdlem79  31922  fourierdlem81  31924  fourierdlem83  31926  fourierdlem92  31935  fourierdlem94  31937  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem113  31956  etransclem2  31973  etransclem46  32017  bnj1326  33950