Theorem chvarvv 2000

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969

This theorem depends on definitions:  df-bi 206  df-ex 1780

This theorem is referenced by:  axextg  2703  nfcriOLD  2891  nfcriOLDOLD  2892  axrep1  5285  axsepg  5299  tz6.12f  6916  frrlem12  8284  dfac12lem2  10141  wunex2  10735  ltordlem  11743  prodfdiv  15846  iscatd2  17629  yoniso  18242  mndind  18745  gsum2dlem2  19880  isdrngrd  20534  isdrngrdOLD  20536  frlmphl  21555  frlmup1  21572  mdetralt  22330  mdetunilem9  22342  neiptoptop  22855  neiptopnei  22856  cnextcn  23791  cnextfres1  23792  ustuqtop4  23969  dscmet  24301  nrmmetd  24303  rolle  25742  numclwlk2lem2f1o  29899  chscllem2  31158  suppovss  32173  fedgmullem1  33002  esumcvg  33382  eulerpartlemgvv  33673  eulerpartlemn  33678  bnj1326  34335  fwddifnp1  35441  poimirlem13  36804  poimirlem14  36805  poimirlem25  36816  poimirlem31  36822  ftc1anclem7  36870  ftc1anc  36872  fdc  36916  fdc1  36917  iscringd  37169  sticksstones2  41269  ismrcd2  41739  fphpdo  41857  monotoddzzfi  41983  monotoddzz  41984  mendlmod  42237  dvgrat  43373  cvgdvgrat  43374  binomcxplemnotnn0  43417  iunincfi  44084  wessf1ornlem  44182  monoords  44305  limcperiod  44642  sumnnodd  44644  cncfshift  44888  cncfperiod  44893  icccncfext  44901  fperdvper  44933  dvnprodlem1  44960  dvnprodlem2  44961  dvnprodlem3  44962  iblspltprt  44987  itgspltprt  44993  stoweidlem43  45057  stoweidlem62  45076  dirkercncflem2  45118  fourierdlem12  45133  fourierdlem15  45136  fourierdlem34  45155  fourierdlem41  45162  fourierdlem42  45163  fourierdlem48  45168  fourierdlem50  45170  fourierdlem51  45171  fourierdlem73  45193  fourierdlem79  45199  fourierdlem81  45201  fourierdlem83  45203  fourierdlem92  45212  fourierdlem94  45214  fourierdlem103  45223  fourierdlem104  45224  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  etransclem2  45250  etransclem46  45294  intsaluni  45343  meaiuninclem  45494  meaiuninc3v  45498  meaiininclem  45500  ovn0lem  45579  hoidmvlelem2  45610  hoidmvlelem3  45611  hspmbllem2  45641  vonioo  45696  vonicc  45699  pimincfltioc  45730  smflimlem3  45787  smflimlem4  45788