Theorem chvarvv 2012

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  axextg  2739  axrep1  5233  axsepg  5252  tz6.12f  6896  frrlem12  8282  dfac12lem2  10116  wunex2  10711  ltordlem  11727  prodfdiv  15940  iscatd2  17727  yoniso  18331  mndind  18877  gsum2dlem2  20032  isdrngrd  20839  isdrngrdOLD  20841  frlmphl  21891  frlmup1  21908  mdetralt  22726  mdetunilem9  22738  neiptoptop  23249  neiptopnei  23250  cnextcn  24185  cnextfres1  24186  ustuqtop4  24362  dscmet  24690  nrmmetd  24692  rolle  26110  numclwlk2lem2f1o  30639  chscllem2  31899  suppovss  32938  fedgmullem1  33936  esumcvg  34393  eulerpartlemgvv  34683  eulerpartlemn  34688  bnj1326  35331  fwddifnp1  36528  axtco1  36846  axtco1from2  36848  poimirlem13  38144  poimirlem14  38145  poimirlem25  38156  poimirlem31  38162  ftc1anclem7  38210  ftc1anc  38212  fdc  38256  fdc1  38257  iscringd  38509  sticksstones2  42776  ismrcd2  43292  fphpdo  43406  monotoddzzfi  43531  monotoddzz  43532  mendlmod  43778  dvgrat  44886  cvgdvgrat  44887  binomcxplemnotnn0  44930  iunincfi  45670  wessf1ornlem  45761  monoords  45874  limcperiod  46202  sumnnodd  46204  cncfshift  46446  cncfperiod  46451  icccncfext  46459  fperdvper  46491  dvnprodlem1  46518  dvnprodlem2  46519  dvnprodlem3  46520  iblspltprt  46545  itgspltprt  46551  stoweidlem43  46615  stoweidlem62  46634  dirkercncflem2  46676  fourierdlem12  46691  fourierdlem15  46694  fourierdlem34  46713  fourierdlem41  46720  fourierdlem42  46721  fourierdlem48  46726  fourierdlem50  46728  fourierdlem51  46729  fourierdlem73  46751  fourierdlem79  46757  fourierdlem81  46759  fourierdlem83  46761  fourierdlem92  46770  fourierdlem94  46772  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem112  46790  fourierdlem113  46791  etransclem2  46808  etransclem46  46852  intsaluni  46901  meaiuninclem  47052  meaiuninc3v  47056  meaiininclem  47058  ovn0lem  47137  hoidmvlelem2  47168  hoidmvlelem3  47169  hspmbllem2  47199  vonioo  47254  vonicc  47257  pimincfltioc  47288  smflimlem3  47345  smflimlem4  47346