Theorem chvarv 1983

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 1683	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 1982	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 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-13 1968

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

This theorem is referenced by:  axext3OLD  2448  axrep1  4559  axsep2  4569  isso2i  4832  tz6.12f  5884  dfac12lem2  8524  wunex2  9116  ltordlem  10078  iscatd2  14936  yoniso  15412  mrcmndind  15816  gsum2dlem2  16801  gsum2dOLD  16803  isdrngrd  17222  frlmphl  18607  frlmup1  18627  mdetralt  18905  mdetunilem9  18917  neiptoptop  19426  neiptopnei  19427  cnextcn  20330  cnextfres  20331  ustuqtop4  20510  dscmet  20856  nrmmetd  20858  rolle  22154  numclwlk2lem2f1o  24810  chscllem2  26260  esumcvg  27760  eulerpartlemgvv  27983  eulerpartlemn  27988  prodfdiv  28635  ftc1anclem7  29701  ftc1anc  29703  fdc  29869  fdc1  29870  iscringd  30027  ismrcd2  30263  fphpdo  30383  monotoddzzfi  30510  monotoddzz  30511  mendlmod  30775  sumnnodd  31200  fperdvper  31276  stoweidlem43  31371  stoweidlem62  31390  fourierdlem12  31447  fourierdlem41  31476  fourierdlem48  31483  fourierdlem51  31486  fourierdlem83  31518  fourierdlem94  31529  fourierdlem111  31546  fourierdlem112  31547  fourierdlem113  31548  bnj1326  33179