Theorem chvarvv 1991

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2401 with a disjoint variable condition, which does not require ax-13 2377. (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  2711  axrep1  5227  axsepg  5244  tz6.12f  6867  frrlem12  8249  dfac12lem2  10067  wunex2  10661  ltordlem  11674  prodfdiv  15831  iscatd2  17616  yoniso  18220  mndind  18765  gsum2dlem2  19912  isdrngrd  20711  isdrngrdOLD  20713  frlmphl  21748  frlmup1  21765  mdetralt  22564  mdetunilem9  22576  neiptoptop  23087  neiptopnei  23088  cnextcn  24023  cnextfres1  24024  ustuqtop4  24200  dscmet  24528  nrmmetd  24530  rolle  25962  numclwlk2lem2f1o  30466  chscllem2  31725  suppovss  32770  fedgmullem1  33806  esumcvg  34263  eulerpartlemgvv  34553  eulerpartlemn  34558  bnj1326  35201  fwddifnp1  36378  poimirlem13  37878  poimirlem14  37879  poimirlem25  37890  poimirlem31  37896  ftc1anclem7  37944  ftc1anc  37946  fdc  37990  fdc1  37991  iscringd  38243  sticksstones2  42511  ismrcd2  43050  fphpdo  43168  monotoddzzfi  43293  monotoddzz  43294  mendlmod  43540  dvgrat  44662  cvgdvgrat  44663  binomcxplemnotnn0  44706  iunincfi  45447  wessf1ornlem  45538  monoords  45653  limcperiod  45982  sumnnodd  45984  cncfshift  46226  cncfperiod  46231  icccncfext  46239  fperdvper  46271  dvnprodlem1  46298  dvnprodlem2  46299  dvnprodlem3  46300  iblspltprt  46325  itgspltprt  46331  stoweidlem43  46395  stoweidlem62  46414  dirkercncflem2  46456  fourierdlem12  46471  fourierdlem15  46474  fourierdlem34  46493  fourierdlem41  46500  fourierdlem42  46501  fourierdlem48  46506  fourierdlem50  46508  fourierdlem51  46509  fourierdlem73  46531  fourierdlem79  46537  fourierdlem81  46539  fourierdlem83  46541  fourierdlem92  46550  fourierdlem94  46552  fourierdlem103  46561  fourierdlem104  46562  fourierdlem111  46569  fourierdlem112  46570  fourierdlem113  46571  etransclem2  46588  etransclem46  46632  intsaluni  46681  meaiuninclem  46832  meaiuninc3v  46836  meaiininclem  46838  ovn0lem  46917  hoidmvlelem2  46948  hoidmvlelem3  46949  hspmbllem2  46979  vonioo  47034  vonicc  47037  pimincfltioc  47068  smflimlem3  47125  smflimlem4  47126