Theorem chvarvv 2022

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 2021	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1830	1 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  axextg  2735  axrep1  5233  axsepg  5250  tz6.12f  6902  frrlem12  8299  dfac12lem2  10204  wunex2  10804  ltordlem  11822  prodfdiv  16045  iscatd2  17835  yoniso  18439  mndind  19004  gsum2dlem2  20165  isdrngrd  21003  isdrngrdOLD  21005  frlmphl  22067  frlmup1  22084  mdetralt  22903  mdetunilem9  22915  neiptoptop  23429  neiptopnei  23430  cnextcn  24366  cnextfres1  24367  ustuqtop4  24543  dscmet  24871  nrmmetd  24873  rolle  26290  numclwlk2lem2f1o  30962  chscllem2  32222  suppovss  33256  fedgmullem1  34243  esumcvg  34700  eulerpartlemgvv  34991  eulerpartlemn  34996  bnj1326  35639  fwddifnp1  36900  axtco1  37231  axtco1from2  37233  poimirlem13  38519  poimirlem14  38520  poimirlem25  38531  poimirlem31  38537  ftc1anclem7  38585  ftc1anc  38587  fdc  38647  fdc1  38648  iscringd  38900  sticksstones2  43165  ismrcd2  43663  fphpdo  43777  monotoddzzfi  43902  monotoddzz  43903  mendlmod  44149  dvgrat  45255  cvgdvgrat  45256  binomcxplemnotnn0  45299  iunincfi  46052  wessf1ornlem  46143  monoords  46256  limcperiod  46584  sumnnodd  46586  cncfshift  46828  cncfperiod  46833  icccncfext  46841  fperdvper  46873  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  iblspltprt  46927  itgspltprt  46933  stoweidlem43  46997  stoweidlem62  47016  dirkercncflem2  47058  fourierdlem12  47073  fourierdlem15  47076  fourierdlem34  47095  fourierdlem41  47102  fourierdlem42  47103  fourierdlem48  47108  fourierdlem50  47110  fourierdlem51  47111  fourierdlem73  47133  fourierdlem79  47139  fourierdlem81  47141  fourierdlem83  47143  fourierdlem92  47152  fourierdlem94  47154  fourierdlem103  47163  fourierdlem104  47164  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  etransclem2  47190  etransclem46  47234  intsaluni  47283  meaiuninclem  47434  meaiuninc3v  47438  meaiininclem  47440  ovn0lem  47519  hoidmvlelem2  47550  hoidmvlelem3  47551  hspmbllem2  47581  vonioo  47636  vonicc  47639  pimincfltioc  47670  smflimlem3  47727  smflimlem4  47728