Theorem chvarvv 2006

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 2004	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1804	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 1802  ax-4 1816  ax-5 1917  ax-6 1975

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

This theorem is referenced by:  axextg  2713  nfcriOLD  2899  nfcriOLDOLD  2900  axrep1  5215  axsepg  5228  tz6.12f  6795  frrlem12  8105  dfac12lem2  9911  wunex2  10505  ltordlem  11511  prodfdiv  15619  iscatd2  17401  yoniso  18014  mndind  18477  gsum2dlem2  19583  isdrngrd  20028  frlmphl  20999  frlmup1  21016  mdetralt  21768  mdetunilem9  21780  neiptoptop  22293  neiptopnei  22294  cnextcn  23229  cnextfres1  23230  ustuqtop4  23407  dscmet  23739  nrmmetd  23741  rolle  25165  numclwlk2lem2f1o  28752  chscllem2  30009  suppovss  31026  fedgmullem1  31719  esumcvg  32063  eulerpartlemgvv  32352  eulerpartlemn  32357  bnj1326  33015  fwddifnp1  34476  poimirlem13  35799  poimirlem14  35800  poimirlem25  35811  poimirlem31  35817  ftc1anclem7  35865  ftc1anc  35867  fdc  35912  fdc1  35913  iscringd  36165  sticksstones2  40112  ismrcd2  40530  fphpdo  40648  monotoddzzfi  40773  monotoddzz  40774  mendlmod  41027  dvgrat  41912  cvgdvgrat  41913  binomcxplemnotnn0  41956  iunincfi  42626  wessf1ornlem  42704  monoords  42818  limcperiod  43151  sumnnodd  43153  cncfshift  43397  cncfperiod  43402  icccncfext  43410  fperdvper  43442  dvnprodlem1  43469  dvnprodlem2  43470  dvnprodlem3  43471  iblspltprt  43496  itgspltprt  43502  stoweidlem43  43566  stoweidlem62  43585  dirkercncflem2  43627  fourierdlem12  43642  fourierdlem15  43645  fourierdlem34  43664  fourierdlem41  43671  fourierdlem42  43672  fourierdlem48  43677  fourierdlem50  43679  fourierdlem51  43680  fourierdlem73  43702  fourierdlem79  43708  fourierdlem81  43710  fourierdlem83  43712  fourierdlem92  43721  fourierdlem94  43723  fourierdlem103  43732  fourierdlem104  43733  fourierdlem111  43740  fourierdlem112  43741  fourierdlem113  43742  etransclem2  43759  etransclem46  43803  intsaluni  43850  meaiuninclem  44000  meaiuninc3v  44004  meaiininclem  44006  ovn0lem  44085  hoidmvlelem2  44116  hoidmvlelem3  44117  hspmbllem2  44147  vonioo  44202  vonicc  44205  pimincfltioc  44232  smflimlem3  44287  smflimlem4  44288