Theorem chvarvv 1998

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1778

This theorem is referenced by:  axextg  2713  axrep1  5304  axsepg  5318  tz6.12f  6946  frrlem12  8338  dfac12lem2  10214  wunex2  10807  ltordlem  11815  prodfdiv  15944  iscatd2  17739  yoniso  18355  mndind  18863  gsum2dlem2  20013  isdrngrd  20788  isdrngrdOLD  20790  frlmphl  21824  frlmup1  21841  mdetralt  22635  mdetunilem9  22647  neiptoptop  23160  neiptopnei  23161  cnextcn  24096  cnextfres1  24097  ustuqtop4  24274  dscmet  24606  nrmmetd  24608  rolle  26048  numclwlk2lem2f1o  30411  chscllem2  31670  suppovss  32697  fedgmullem1  33642  esumcvg  34050  eulerpartlemgvv  34341  eulerpartlemn  34346  bnj1326  35002  fwddifnp1  36129  poimirlem13  37593  poimirlem14  37594  poimirlem25  37605  poimirlem31  37611  ftc1anclem7  37659  ftc1anc  37661  fdc  37705  fdc1  37706  iscringd  37958  sticksstones2  42104  ismrcd2  42655  fphpdo  42773  monotoddzzfi  42899  monotoddzz  42900  mendlmod  43150  dvgrat  44281  cvgdvgrat  44282  binomcxplemnotnn0  44325  iunincfi  44996  wessf1ornlem  45092  monoords  45212  limcperiod  45549  sumnnodd  45551  cncfshift  45795  cncfperiod  45800  icccncfext  45808  fperdvper  45840  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  iblspltprt  45894  itgspltprt  45900  stoweidlem43  45964  stoweidlem62  45983  dirkercncflem2  46025  fourierdlem12  46040  fourierdlem15  46043  fourierdlem34  46062  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem50  46077  fourierdlem51  46078  fourierdlem73  46100  fourierdlem79  46106  fourierdlem81  46108  fourierdlem83  46110  fourierdlem92  46119  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  etransclem2  46157  etransclem46  46201  intsaluni  46250  meaiuninclem  46401  meaiuninc3v  46405  meaiininclem  46407  ovn0lem  46486  hoidmvlelem2  46517  hoidmvlelem3  46518  hspmbllem2  46548  vonioo  46603  vonicc  46606  pimincfltioc  46637  smflimlem3  46694  smflimlem4  46695