Theorem chvarvv 2012

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2430 with a disjoint variable condition, which does not require ax-13 2406. (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 2011	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1820	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  axextg  2739  axrep1  5232  axsepg  5251  tz6.12f  6896  frrlem12  8282  dfac12lem2  10116  wunex2  10711  ltordlem  11727  prodfdiv  15938  iscatd2  17725  yoniso  18329  mndind  18875  gsum2dlem2  20029  isdrngrd  20836  isdrngrdOLD  20838  frlmphl  21888  frlmup1  21905  mdetralt  22722  mdetunilem9  22734  neiptoptop  23245  neiptopnei  23246  cnextcn  24181  cnextfres1  24182  ustuqtop4  24358  dscmet  24686  nrmmetd  24688  rolle  26106  numclwlk2lem2f1o  30635  chscllem2  31895  suppovss  32934  fedgmullem1  33931  esumcvg  34388  eulerpartlemgvv  34678  eulerpartlemn  34683  bnj1326  35326  fwddifnp1  36523  axtco1  36841  axtco1from2  36843  poimirlem13  38139  poimirlem14  38140  poimirlem25  38151  poimirlem31  38157  ftc1anclem7  38205  ftc1anc  38207  fdc  38251  fdc1  38252  iscringd  38504  sticksstones2  42771  ismrcd2  43287  fphpdo  43401  monotoddzzfi  43526  monotoddzz  43527  mendlmod  43773  dvgrat  44881  cvgdvgrat  44882  binomcxplemnotnn0  44925  iunincfi  45671  wessf1ornlem  45762  monoords  45875  limcperiod  46203  sumnnodd  46205  cncfshift  46447  cncfperiod  46452  icccncfext  46460  fperdvper  46492  dvnprodlem1  46519  dvnprodlem2  46520  dvnprodlem3  46521  iblspltprt  46546  itgspltprt  46552  stoweidlem43  46616  stoweidlem62  46635  dirkercncflem2  46677  fourierdlem12  46692  fourierdlem15  46695  fourierdlem34  46714  fourierdlem41  46721  fourierdlem42  46722  fourierdlem48  46727  fourierdlem50  46729  fourierdlem51  46730  fourierdlem73  46752  fourierdlem79  46758  fourierdlem81  46760  fourierdlem83  46762  fourierdlem92  46771  fourierdlem94  46773  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  etransclem2  46809  etransclem46  46853  intsaluni  46902  meaiuninclem  47053  meaiuninc3v  47057  meaiininclem  47059  ovn0lem  47138  hoidmvlelem2  47169  hoidmvlelem3  47170  hspmbllem2  47200  vonioo  47255  vonicc  47258  pimincfltioc  47289  smflimlem3  47346  smflimlem4  47347