Theorem chvarv 1958

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 1673	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 1957	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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590

This theorem is referenced by:  axext3  2425  axrep1  4404  axsep2  4414  isso2i  4673  tz6.12f  5708  dfac12lem2  8313  wunex2  8905  ltordlem  9865  iscatd2  14619  yoniso  15095  mrcmndind  15494  gsum2dlem2  16462  gsum2dOLD  16464  isdrngrd  16858  frlmphl  18206  frlmup1  18226  mdetralt  18414  mdetunilem9  18426  neiptoptop  18735  neiptopnei  18736  cnextcn  19639  cnextfres  19640  ustuqtop4  19819  dscmet  20165  nrmmetd  20167  rolle  21462  chscllem2  25041  esumcvg  26535  eulerpartlemgvv  26759  eulerpartlemn  26764  prodfdiv  27411  ftc1anclem7  28473  ftc1anc  28475  fdc  28641  fdc1  28642  iscringd  28799  ismrcd2  29035  fphpdo  29156  monotoddzzfi  29283  monotoddzz  29284  mendlmod  29550  stoweidlem43  29838  stoweidlem62  29857  numclwlk2lem2f1o  30698  bnj1326  32017