Theorem chvarvv 2005

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

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  axextg  2795  axrep1  5191  axsepg  5204  tz6.12f  6694  dfac12lem2  9570  wunex2  10160  ltordlem  11165  prodfdiv  15252  iscatd2  16952  yoniso  17535  mndind  17992  gsum2dlem2  19091  isdrngrd  19528  frlmphl  20925  frlmup1  20942  mdetralt  21217  mdetunilem9  21229  neiptoptop  21739  neiptopnei  21740  cnextcn  22675  cnextfres1  22676  ustuqtop4  22853  dscmet  23182  nrmmetd  23184  rolle  24587  numclwlk2lem2f1o  28158  chscllem2  29415  suppovss  30426  fedgmullem1  31025  esumcvg  31345  eulerpartlemgvv  31634  eulerpartlemn  31639  bnj1326  32298  frrlem12  33134  fwddifnp1  33626  poimirlem13  34920  poimirlem14  34921  poimirlem25  34932  poimirlem31  34938  ftc1anclem7  34988  ftc1anc  34990  fdc  35035  fdc1  35036  iscringd  35291  ismrcd2  39345  fphpdo  39463  monotoddzzfi  39588  monotoddzz  39589  mendlmod  39842  dvgrat  40693  cvgdvgrat  40694  binomcxplemnotnn0  40737  iunincfi  41409  wessf1ornlem  41494  monoords  41613  limcperiod  41958  sumnnodd  41960  cncfshift  42206  cncfperiod  42211  icccncfext  42219  fperdvper  42252  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  iblspltprt  42307  itgspltprt  42313  stoweidlem43  42377  stoweidlem62  42396  dirkercncflem2  42438  fourierdlem12  42453  fourierdlem15  42456  fourierdlem34  42475  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem50  42490  fourierdlem51  42491  fourierdlem73  42513  fourierdlem79  42519  fourierdlem81  42521  fourierdlem83  42523  fourierdlem92  42532  fourierdlem94  42534  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  etransclem2  42570  etransclem46  42614  intsaluni  42661  meaiuninclem  42811  meaiuninc3v  42815  meaiininclem  42817  ovn0lem  42896  hoidmvlelem2  42927  hoidmvlelem3  42928  hspmbllem2  42958  vonioo  43013  vonicc  43016  pimincfltioc  43043  smflimlem3  43098  smflimlem4  43099