Theorem chvarvv 1991

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2400 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
chvarvv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvarvv.2	⊢ 𝜑

Assertion

Ref	Expression
chvarvv	⊢ 𝜓

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem chvarvv

Step	Hyp	Ref	Expression
1		chvarvv.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	spvv 1990	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1799	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  axextg  2710  axrep1  5213  axsepg  5232  tz6.12f  6865  frrlem12  8247  dfac12lem2  10067  wunex2  10661  ltordlem  11675  prodfdiv  15861  iscatd2  17647  yoniso  18251  mndind  18796  gsum2dlem2  19946  isdrngrd  20743  isdrngrdOLD  20745  frlmphl  21761  frlmup1  21778  mdetralt  22573  mdetunilem9  22585  neiptoptop  23096  neiptopnei  23097  cnextcn  24032  cnextfres1  24033  ustuqtop4  24209  dscmet  24537  nrmmetd  24539  rolle  25957  numclwlk2lem2f1o  30449  chscllem2  31709  suppovss  32754  fedgmullem1  33773  esumcvg  34230  eulerpartlemgvv  34520  eulerpartlemn  34525  bnj1326  35168  fwddifnp1  36347  axtco1  36655  axtco1from2  36657  poimirlem13  37954  poimirlem14  37955  poimirlem25  37966  poimirlem31  37972  ftc1anclem7  38020  ftc1anc  38022  fdc  38066  fdc1  38067  iscringd  38319  sticksstones2  42586  ismrcd2  43131  fphpdo  43245  monotoddzzfi  43370  monotoddzz  43371  mendlmod  43617  dvgrat  44739  cvgdvgrat  44740  binomcxplemnotnn0  44783  iunincfi  45524  wessf1ornlem  45615  monoords  45730  limcperiod  46058  sumnnodd  46060  cncfshift  46302  cncfperiod  46307  icccncfext  46315  fperdvper  46347  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  iblspltprt  46401  itgspltprt  46407  stoweidlem43  46471  stoweidlem62  46490  dirkercncflem2  46532  fourierdlem12  46547  fourierdlem15  46550  fourierdlem34  46569  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem50  46584  fourierdlem51  46585  fourierdlem73  46607  fourierdlem79  46613  fourierdlem81  46615  fourierdlem83  46617  fourierdlem92  46626  fourierdlem94  46628  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  etransclem2  46664  etransclem46  46708  intsaluni  46757  meaiuninclem  46908  meaiuninc3v  46912  meaiininclem  46914  ovn0lem  46993  hoidmvlelem2  47024  hoidmvlelem3  47025  hspmbllem2  47055  vonioo  47110  vonicc  47113  pimincfltioc  47144  smflimlem3  47201  smflimlem4  47202