Theorem chvarvv 2022

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2427 with a disjoint variable condition, which does not require ax-13 2403. (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  2736  axrep1  5237  axsepg  5256  tz6.12f  6907  frrlem12  8300  dfac12lem2  10151  wunex2  10751  ltordlem  11767  prodfdiv  15989  iscatd2  17775  yoniso  18379  mndind  18943  gsum2dlem2  20104  isdrngrd  20938  isdrngrdOLD  20940  frlmphl  22000  frlmup1  22017  mdetralt  22836  mdetunilem9  22848  neiptoptop  23362  neiptopnei  23363  cnextcn  24299  cnextfres1  24300  ustuqtop4  24476  dscmet  24804  nrmmetd  24806  rolle  26224  numclwlk2lem2f1o  30867  chscllem2  32127  suppovss  33161  fedgmullem1  34147  esumcvg  34604  eulerpartlemgvv  34895  eulerpartlemn  34900  bnj1326  35543  fwddifnp1  36753  axtco1  37100  axtco1from2  37102  poimirlem13  38390  poimirlem14  38391  poimirlem25  38402  poimirlem31  38408  ftc1anclem7  38456  ftc1anc  38458  fdc  38503  fdc1  38504  iscringd  38756  sticksstones2  43021  ismrcd2  43552  fphpdo  43666  monotoddzzfi  43791  monotoddzz  43792  mendlmod  44038  dvgrat  45144  cvgdvgrat  45145  binomcxplemnotnn0  45188  iunincfi  45934  wessf1ornlem  46025  monoords  46138  limcperiod  46466  sumnnodd  46468  cncfshift  46710  cncfperiod  46715  icccncfext  46723  fperdvper  46755  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  iblspltprt  46809  itgspltprt  46815  stoweidlem43  46879  stoweidlem62  46898  dirkercncflem2  46940  fourierdlem12  46955  fourierdlem15  46958  fourierdlem34  46977  fourierdlem41  46984  fourierdlem42  46985  fourierdlem48  46990  fourierdlem50  46992  fourierdlem51  46993  fourierdlem73  47015  fourierdlem79  47021  fourierdlem81  47023  fourierdlem83  47025  fourierdlem92  47034  fourierdlem94  47036  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  etransclem2  47072  etransclem46  47116  intsaluni  47165  meaiuninclem  47316  meaiuninc3v  47320  meaiininclem  47322  ovn0lem  47401  hoidmvlelem2  47432  hoidmvlelem3  47433  hspmbllem2  47463  vonioo  47518  vonicc  47521  pimincfltioc  47552  smflimlem3  47609  smflimlem4  47610