Theorem chvarvv 2008

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

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  axextg  2735  axrep1  5227  axsepg  5246  tz6.12f  6888  frrlem12  8273  dfac12lem2  10098  wunex2  10693  ltordlem  11709  prodfdiv  15909  iscatd2  17696  yoniso  18300  mndind  18845  gsum2dlem2  19994  isdrngrd  20795  isdrngrdOLD  20797  frlmphl  21813  frlmup1  21830  mdetralt  22648  mdetunilem9  22660  neiptoptop  23171  neiptopnei  23172  cnextcn  24107  cnextfres1  24108  ustuqtop4  24284  dscmet  24612  nrmmetd  24614  rolle  26032  numclwlk2lem2f1o  30527  chscllem2  31787  suppovss  32833  fedgmullem1  33887  esumcvg  34344  eulerpartlemgvv  34634  eulerpartlemn  34639  bnj1326  35285  fwddifnp1  36479  axtco1  36797  axtco1from2  36799  poimirlem13  38096  poimirlem14  38097  poimirlem25  38108  poimirlem31  38114  ftc1anclem7  38162  ftc1anc  38164  fdc  38208  fdc1  38209  iscringd  38461  sticksstones2  42728  ismrcd2  43244  fphpdo  43358  monotoddzzfi  43483  monotoddzz  43484  mendlmod  43730  dvgrat  44852  cvgdvgrat  44853  binomcxplemnotnn0  44896  iunincfi  45636  wessf1ornlem  45727  monoords  45840  limcperiod  46168  sumnnodd  46170  cncfshift  46412  cncfperiod  46417  icccncfext  46425  fperdvper  46457  dvnprodlem1  46484  dvnprodlem2  46485  dvnprodlem3  46486  iblspltprt  46511  itgspltprt  46517  stoweidlem43  46581  stoweidlem62  46600  dirkercncflem2  46642  fourierdlem12  46657  fourierdlem15  46660  fourierdlem34  46679  fourierdlem41  46686  fourierdlem42  46687  fourierdlem48  46692  fourierdlem50  46694  fourierdlem51  46695  fourierdlem73  46717  fourierdlem79  46723  fourierdlem81  46725  fourierdlem83  46727  fourierdlem92  46736  fourierdlem94  46738  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierdlem112  46756  fourierdlem113  46757  etransclem2  46774  etransclem46  46818  intsaluni  46867  meaiuninclem  47018  meaiuninc3v  47022  meaiininclem  47024  ovn0lem  47103  hoidmvlelem2  47134  hoidmvlelem3  47135  hspmbllem2  47165  vonioo  47220  vonicc  47223  pimincfltioc  47254  smflimlem3  47311  smflimlem4  47312