Theorem chvarvv 2019

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2428 with a disjoint variable condition, which does not require ax-13 2404. (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 2018	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1827	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 1825  ax-4 1839  ax-5 1940  ax-6 1997

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

This theorem is referenced by:  axextg  2737  axrep1  5240  axsepg  5259  tz6.12f  6908  frrlem12  8295  dfac12lem2  10129  wunex2  10724  ltordlem  11740  prodfdiv  15952  iscatd2  17738  yoniso  18342  mndind  18888  gsum2dlem2  20042  isdrngrd  20851  isdrngrdOLD  20853  frlmphl  21912  frlmup1  21929  mdetralt  22746  mdetunilem9  22758  neiptoptop  23269  neiptopnei  23270  cnextcn  24205  cnextfres1  24206  ustuqtop4  24382  dscmet  24710  nrmmetd  24712  rolle  26130  numclwlk2lem2f1o  30711  chscllem2  31971  suppovss  33007  fedgmullem1  34000  esumcvg  34457  eulerpartlemgvv  34747  eulerpartlemn  34752  bnj1326  35395  fwddifnp1  36638  axtco1  36965  axtco1from2  36967  poimirlem13  38265  poimirlem14  38266  poimirlem25  38277  poimirlem31  38283  ftc1anclem7  38331  ftc1anc  38333  fdc  38377  fdc1  38378  iscringd  38630  sticksstones2  42895  ismrcd2  43413  fphpdo  43527  monotoddzzfi  43652  monotoddzz  43653  mendlmod  43899  dvgrat  45005  cvgdvgrat  45006  binomcxplemnotnn0  45049  iunincfi  45795  wessf1ornlem  45886  monoords  45999  limcperiod  46327  sumnnodd  46329  cncfshift  46571  cncfperiod  46576  icccncfext  46584  fperdvper  46616  dvnprodlem1  46643  dvnprodlem2  46644  dvnprodlem3  46645  iblspltprt  46670  itgspltprt  46676  stoweidlem43  46740  stoweidlem62  46759  dirkercncflem2  46801  fourierdlem12  46816  fourierdlem15  46819  fourierdlem34  46838  fourierdlem41  46845  fourierdlem42  46846  fourierdlem48  46851  fourierdlem50  46853  fourierdlem51  46854  fourierdlem73  46876  fourierdlem79  46882  fourierdlem81  46884  fourierdlem83  46886  fourierdlem92  46895  fourierdlem94  46897  fourierdlem103  46906  fourierdlem104  46907  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  etransclem2  46933  etransclem46  46977  intsaluni  47026  meaiuninclem  47177  meaiuninc3v  47181  meaiininclem  47183  ovn0lem  47262  hoidmvlelem2  47293  hoidmvlelem3  47294  hspmbllem2  47324  vonioo  47379  vonicc  47382  pimincfltioc  47413  smflimlem3  47470  smflimlem4  47471