Theorem chvarvv 2003

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  axextg  2706  nfcriOLD  2894  nfcriOLDOLD  2895  axrep1  5287  axsepg  5301  tz6.12f  6918  frrlem12  8282  dfac12lem2  10139  wunex2  10733  ltordlem  11739  prodfdiv  15842  iscatd2  17625  yoniso  18238  mndind  18709  gsum2dlem2  19839  isdrngrd  20391  isdrngrdOLD  20393  frlmphl  21336  frlmup1  21353  mdetralt  22110  mdetunilem9  22122  neiptoptop  22635  neiptopnei  22636  cnextcn  23571  cnextfres1  23572  ustuqtop4  23749  dscmet  24081  nrmmetd  24083  rolle  25507  numclwlk2lem2f1o  29632  chscllem2  30891  suppovss  31906  fedgmullem1  32714  esumcvg  33084  eulerpartlemgvv  33375  eulerpartlemn  33380  bnj1326  34037  fwddifnp1  35137  poimirlem13  36501  poimirlem14  36502  poimirlem25  36513  poimirlem31  36519  ftc1anclem7  36567  ftc1anc  36569  fdc  36613  fdc1  36614  iscringd  36866  sticksstones2  40963  ismrcd2  41437  fphpdo  41555  monotoddzzfi  41681  monotoddzz  41682  mendlmod  41935  dvgrat  43071  cvgdvgrat  43072  binomcxplemnotnn0  43115  iunincfi  43783  wessf1ornlem  43882  monoords  44007  limcperiod  44344  sumnnodd  44346  cncfshift  44590  cncfperiod  44595  icccncfext  44603  fperdvper  44635  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  iblspltprt  44689  itgspltprt  44695  stoweidlem43  44759  stoweidlem62  44778  dirkercncflem2  44820  fourierdlem12  44835  fourierdlem15  44838  fourierdlem34  44857  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem50  44872  fourierdlem51  44873  fourierdlem73  44895  fourierdlem79  44901  fourierdlem81  44903  fourierdlem83  44905  fourierdlem92  44914  fourierdlem94  44916  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  etransclem2  44952  etransclem46  44996  intsaluni  45045  meaiuninclem  45196  meaiuninc3v  45200  meaiininclem  45202  ovn0lem  45281  hoidmvlelem2  45312  hoidmvlelem3  45313  hspmbllem2  45343  vonioo  45398  vonicc  45401  pimincfltioc  45432  smflimlem3  45489  smflimlem4  45490