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  5286  axsepg  5300  tz6.12f  6915  frrlem12  8279  dfac12lem2  10136  wunex2  10730  ltordlem  11736  prodfdiv  15839  iscatd2  17622  yoniso  18235  mndind  18706  gsum2dlem2  19834  isdrngrd  20342  isdrngrdOLD  20344  frlmphl  21328  frlmup1  21345  mdetralt  22102  mdetunilem9  22114  neiptoptop  22627  neiptopnei  22628  cnextcn  23563  cnextfres1  23564  ustuqtop4  23741  dscmet  24073  nrmmetd  24075  rolle  25499  numclwlk2lem2f1o  29622  chscllem2  30879  suppovss  31894  fedgmullem1  32703  esumcvg  33073  eulerpartlemgvv  33364  eulerpartlemn  33369  bnj1326  34026  fwddifnp1  35126  poimirlem13  36490  poimirlem14  36491  poimirlem25  36502  poimirlem31  36508  ftc1anclem7  36556  ftc1anc  36558  fdc  36602  fdc1  36603  iscringd  36855  sticksstones2  40952  ismrcd2  41423  fphpdo  41541  monotoddzzfi  41667  monotoddzz  41668  mendlmod  41921  dvgrat  43057  cvgdvgrat  43058  binomcxplemnotnn0  43101  iunincfi  43769  wessf1ornlem  43868  monoords  43994  limcperiod  44331  sumnnodd  44333  cncfshift  44577  cncfperiod  44582  icccncfext  44590  fperdvper  44622  dvnprodlem1  44649  dvnprodlem2  44650  dvnprodlem3  44651  iblspltprt  44676  itgspltprt  44682  stoweidlem43  44746  stoweidlem62  44765  dirkercncflem2  44807  fourierdlem12  44822  fourierdlem15  44825  fourierdlem34  44844  fourierdlem41  44851  fourierdlem42  44852  fourierdlem48  44857  fourierdlem50  44859  fourierdlem51  44860  fourierdlem73  44882  fourierdlem79  44888  fourierdlem81  44890  fourierdlem83  44892  fourierdlem92  44901  fourierdlem94  44903  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  etransclem2  44939  etransclem46  44983  intsaluni  45032  meaiuninclem  45183  meaiuninc3v  45187  meaiininclem  45189  ovn0lem  45268  hoidmvlelem2  45299  hoidmvlelem3  45300  hspmbllem2  45330  vonioo  45385  vonicc  45388  pimincfltioc  45419  smflimlem3  45476  smflimlem4  45477