Theorem chvarvv 2002

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 2000	. 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 1913  ax-6 1971

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

This theorem is referenced by:  axextg  2711  nfcriOLD  2897  nfcriOLDOLD  2898  axrep1  5210  axsepg  5224  tz6.12f  6798  frrlem12  8113  dfac12lem2  9900  wunex2  10494  ltordlem  11500  prodfdiv  15608  iscatd2  17390  yoniso  18003  mndind  18466  gsum2dlem2  19572  isdrngrd  20017  frlmphl  20988  frlmup1  21005  mdetralt  21757  mdetunilem9  21769  neiptoptop  22282  neiptopnei  22283  cnextcn  23218  cnextfres1  23219  ustuqtop4  23396  dscmet  23728  nrmmetd  23730  rolle  25154  numclwlk2lem2f1o  28743  chscllem2  30000  suppovss  31017  fedgmullem1  31710  esumcvg  32054  eulerpartlemgvv  32343  eulerpartlemn  32348  bnj1326  33006  fwddifnp1  34467  poimirlem13  35790  poimirlem14  35791  poimirlem25  35802  poimirlem31  35808  ftc1anclem7  35856  ftc1anc  35858  fdc  35903  fdc1  35904  iscringd  36156  sticksstones2  40103  ismrcd2  40521  fphpdo  40639  monotoddzzfi  40764  monotoddzz  40765  mendlmod  41018  dvgrat  41930  cvgdvgrat  41931  binomcxplemnotnn0  41974  iunincfi  42644  wessf1ornlem  42722  monoords  42836  limcperiod  43169  sumnnodd  43171  cncfshift  43415  cncfperiod  43420  icccncfext  43428  fperdvper  43460  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  iblspltprt  43514  itgspltprt  43520  stoweidlem43  43584  stoweidlem62  43603  dirkercncflem2  43645  fourierdlem12  43660  fourierdlem15  43663  fourierdlem34  43682  fourierdlem41  43689  fourierdlem42  43690  fourierdlem48  43695  fourierdlem50  43697  fourierdlem51  43698  fourierdlem73  43720  fourierdlem79  43726  fourierdlem81  43728  fourierdlem83  43730  fourierdlem92  43739  fourierdlem94  43741  fourierdlem103  43750  fourierdlem104  43751  fourierdlem111  43758  fourierdlem112  43759  fourierdlem113  43760  etransclem2  43777  etransclem46  43821  intsaluni  43868  meaiuninclem  44018  meaiuninc3v  44022  meaiininclem  44024  ovn0lem  44103  hoidmvlelem2  44134  hoidmvlelem3  44135  hspmbllem2  44165  vonioo  44220  vonicc  44223  pimincfltioc  44253  smflimlem3  44308  smflimlem4  44309