Theorem chvarvv 1995

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2398 with a disjoint variable condition, which does not require ax-13 2374. (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 1993	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1793	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 1791  ax-4 1805  ax-5 1907  ax-6 1964

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

This theorem is referenced by:  axextg  2707  axrep1  5285  axsepg  5302  tz6.12f  6932  frrlem12  8320  dfac12lem2  10182  wunex2  10775  ltordlem  11785  prodfdiv  15928  iscatd2  17725  yoniso  18341  mndind  18853  gsum2dlem2  20003  isdrngrd  20782  isdrngrdOLD  20784  frlmphl  21818  frlmup1  21835  mdetralt  22629  mdetunilem9  22641  neiptoptop  23154  neiptopnei  23155  cnextcn  24090  cnextfres1  24091  ustuqtop4  24268  dscmet  24600  nrmmetd  24602  rolle  26042  numclwlk2lem2f1o  30407  chscllem2  31666  suppovss  32695  fedgmullem1  33656  esumcvg  34066  eulerpartlemgvv  34357  eulerpartlemn  34362  bnj1326  35018  fwddifnp1  36146  poimirlem13  37619  poimirlem14  37620  poimirlem25  37631  poimirlem31  37637  ftc1anclem7  37685  ftc1anc  37687  fdc  37731  fdc1  37732  iscringd  37984  sticksstones2  42128  ismrcd2  42686  fphpdo  42804  monotoddzzfi  42930  monotoddzz  42931  mendlmod  43177  dvgrat  44307  cvgdvgrat  44308  binomcxplemnotnn0  44351  iunincfi  45033  wessf1ornlem  45127  monoords  45247  limcperiod  45583  sumnnodd  45585  cncfshift  45829  cncfperiod  45834  icccncfext  45842  fperdvper  45874  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  iblspltprt  45928  itgspltprt  45934  stoweidlem43  45998  stoweidlem62  46017  dirkercncflem2  46059  fourierdlem12  46074  fourierdlem15  46077  fourierdlem34  46096  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem50  46111  fourierdlem51  46112  fourierdlem73  46134  fourierdlem79  46140  fourierdlem81  46142  fourierdlem83  46144  fourierdlem92  46153  fourierdlem94  46155  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  etransclem2  46191  etransclem46  46235  intsaluni  46284  meaiuninclem  46435  meaiuninc3v  46439  meaiininclem  46441  ovn0lem  46520  hoidmvlelem2  46551  hoidmvlelem3  46552  hspmbllem2  46582  vonioo  46637  vonicc  46640  pimincfltioc  46671  smflimlem3  46728  smflimlem4  46729