Theorem chvarv 2117

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 1771	. 2 |- F/ x ps
2		chvarv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
3		chvarv.2	. 2 |- ph
4	1, 2, 3	chvar 2116	1 |- ps

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943  ax-13 2101

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678

This theorem is referenced by:  axext3ALT  2444  axrep1  4529  axsep2  4539  isso2i  4805  tz6.12f  5905  dfac12lem2  8599  wunex2  9188  ltordlem  10166  prodfdiv  14000  iscatd2  15635  yoniso  16218  mrcmndind  16661  gsum2dlem2  17651  isdrngrd  18049  frlmphl  19387  frlmup1  19404  mdetralt  19681  mdetunilem9  19693  neiptoptop  20195  neiptopnei  20196  cnextcn  21130  cnextfres1  21131  ustuqtop4  21307  dscmet  21635  nrmmetd  21637  rolle  22990  numclwlk2lem2f1o  25881  chscllem2  27339  esumcvg  28955  eulerpartlemgvv  29257  eulerpartlemn  29262  bnj1326  29883  fwddifnp1  30980  poimirlem13  31997  poimirlem14  31998  poimirlem25  32009  poimirlem31  32015  ftc1anclem7  32067  ftc1anc  32069  fdc  32118  fdc1  32119  iscringd  32276  ismrcd2  35585  fphpdo  35704  monotoddzzfi  35834  monotoddzz  35835  mendlmod  36103  dvgrat  36704  cvgdvgrat  36705  binomcxplemnotnn0  36748  wessf1ornlem  37496  monoords  37551  limcperiod  37745  sumnnodd  37747  cncfshift  37788  cncfperiod  37793  icccncfext  37802  fperdvper  37827  dvnprodlem1  37858  dvnprodlem2  37859  dvnprodlem3  37860  iblspltprt  37887  itgspltprt  37893  stoweidlem43  37941  stoweidlem62  37960  stoweidlem62OLD  37961  dirkercncflem2  38003  fourierdlem12  38018  fourierdlem15  38021  fourierdlem34  38041  fourierdlem41  38048  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem48  38055  fourierdlem50  38057  fourierdlem51  38058  fourierdlem73  38080  fourierdlem79  38086  fourierdlem81  38088  fourierdlem83  38090  fourierdlem92  38099  fourierdlem94  38101  fourierdlem103  38110  fourierdlem104  38111  fourierdlem111  38118  fourierdlem112  38119  fourierdlem113  38120  etransclem2  38138  etransclem46  38182  intsaluni  38225  ovn0lem  38424  hoidmvlelem2  38455  hoidmvlelem3  38456  hspmbllem2  38486