Theorem chvarv 1959

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 1674	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 1958	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 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-12 1793  ax-13 1944

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595

This theorem is referenced by:  axext3  2418  axrep1  4394  axsep2  4404  isso2i  4662  tz6.12f  5698  dfac12lem2  8303  wunex2  8895  ltordlem  9855  iscatd2  14604  yoniso  15080  mrcmndind  15478  gsum2dlem2  16438  gsum2dOLD  16440  isdrngrd  16784  frlmphl  18050  frlmup1  18070  mdetralt  18258  mdetunilem9  18270  neiptoptop  18579  neiptopnei  18580  cnextcn  19483  cnextfres  19484  ustuqtop4  19663  dscmet  20009  nrmmetd  20011  rolle  21306  chscllem2  24866  esumcvg  26391  eulerpartlemgvv  26609  eulerpartlemn  26614  prodfdiv  27260  ftc1anclem7  28319  ftc1anc  28321  fdc  28487  fdc1  28488  iscringd  28645  ismrcd2  28882  fphpdo  29003  monotoddzzfi  29130  monotoddzz  29131  mendlmod  29397  stoweidlem43  29686  stoweidlem62  29705  numclwlk2lem2f1o  30546  bnj1326  31759