Theorem chvarvv 2021

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2425 with a disjoint variable condition, which does not require ax-13 2401. (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 2020	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1829	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 1827  ax-4 1841  ax-5 1942  ax-6 1999

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

This theorem is used by:  axextg  2734  axrep1  5232  axsepg  5249  tz6.12f  6910  frrlem12  8318  dfac12lem2  10226  wunex2  10826  ltordlem  11844  prodfdiv  16070  iscatd2  17860  yoniso  18464  mndind  19029  gsum2dlem2  20190  isdrngrd  21028  isdrngrdOLD  21030  frlmphl  22092  frlmup1  22109  mdetralt  22928  mdetunilem9  22940  neiptoptop  23454  neiptopnei  23455  cnextcn  24391  cnextfres1  24392  ustuqtop4  24568  dscmet  24896  nrmmetd  24898  rolle  26315  numclwlk2lem2f1o  30985  chscllem2  32245  suppovss  33321  fedgmullem1  34307  esumcvg  34764  eulerpartlemgvv  35054  eulerpartlemn  35059  bnj1326  35702  fwddifnp1  37022  axtco1  37353  axtco1from2  37355  poimirlem13  38644  poimirlem14  38645  poimirlem25  38656  poimirlem31  38662  ftc1anclem7  38710  ftc1anc  38712  fdc  38772  fdc1  38773  iscringd  39025  sticksstones2  43290  ismrcd2  43803  fphpdo  43917  monotoddzzfi  44042  monotoddzz  44043  mendlmod  44284  dvgrat  45389  cvgdvgrat  45390  binomcxplemnotnn0  45433  iunincfi  46202  wessf1ornlem  46293  monoords  46406  limcperiod  46733  sumnnodd  46735  cncfshift  46977  cncfperiod  46982  icccncfext  46990  fperdvper  47022  dvnprodlem1  47049  dvnprodlem2  47050  dvnprodlem3  47051  iblspltprt  47076  itgspltprt  47082  stoweidlem43  47146  stoweidlem62  47165  dirkercncflem2  47207  fourierdlem12  47222  fourierdlem15  47225  fourierdlem34  47244  fourierdlem41  47251  fourierdlem42  47252  fourierdlem48  47257  fourierdlem50  47259  fourierdlem51  47260  fourierdlem73  47282  fourierdlem79  47288  fourierdlem81  47290  fourierdlem83  47292  fourierdlem92  47301  fourierdlem94  47303  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fourierdlem112  47321  fourierdlem113  47322  etransclem2  47339  etransclem46  47383  intsaluni  47432  meaiuninclem  47583  meaiuninc3v  47587  meaiininclem  47589  ovn0lem  47668  hoidmvlelem2  47699  hoidmvlelem3  47700  hspmbllem2  47730  vonioo  47785  vonicc  47788  pimincfltioc  47819  smflimlem3  47876  smflimlem4  47877