Theorem chvarvv 2024

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  axextg  2737  axrep1  5237  axsepg  5254  tz6.12f  6936  frrlem12  8346  dfac12lem2  10253  wunex2  10853  ltordlem  11871  prodfdiv  16097  iscatd2  17887  yoniso  18491  mndind  19056  gsum2dlem2  20218  isdrngrd  21056  isdrngrdOLD  21058  frlmphl  22120  frlmup1  22137  mdetralt  22956  mdetunilem9  22968  neiptoptop  23482  neiptopnei  23483  cnextcn  24419  cnextfres1  24420  ustuqtop4  24596  dscmet  24924  nrmmetd  24926  rolle  26343  numclwlk2lem2f1o  31013  chscllem2  32273  suppovss  33348  fedgmullem1  34344  esumcvg  34801  eulerpartlemgvv  35091  eulerpartlemn  35096  bnj1326  35739  fwddifnp1  37121  axtco1  37452  axtco1from2  37454  poimirlem13  38756  poimirlem14  38757  poimirlem25  38768  poimirlem31  38774  ftc1anclem7  38822  ftc1anc  38824  fdc  38882  fdc1  38883  iscringd  39135  sticksstones2  43400  ismrcd2  43914  fphpdo  44028  monotoddzzfi  44153  monotoddzz  44154  mendlmod  44394  dvgrat  45499  cvgdvgrat  45500  binomcxplemnotnn0  45543  iunincfi  46324  wessf1ornlem  46415  monoords  46528  limcperiod  46855  sumnnodd  46857  cncfshift  47099  cncfperiod  47104  icccncfext  47112  fperdvper  47144  dvnprodlem1  47171  dvnprodlem2  47172  dvnprodlem3  47173  iblspltprt  47198  itgspltprt  47204  stoweidlem43  47268  stoweidlem62  47287  dirkercncflem2  47329  fourierdlem12  47344  fourierdlem15  47347  fourierdlem34  47366  fourierdlem41  47373  fourierdlem42  47374  fourierdlem48  47379  fourierdlem50  47381  fourierdlem51  47382  fourierdlem73  47404  fourierdlem79  47410  fourierdlem81  47412  fourierdlem83  47414  fourierdlem92  47423  fourierdlem94  47425  fourierdlem103  47434  fourierdlem104  47435  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  etransclem2  47461  etransclem46  47505  intsaluni  47554  meaiuninclem  47705  meaiuninc3v  47709  meaiininclem  47711  ovn0lem  47790  hoidmvlelem2  47821  hoidmvlelem3  47822  hspmbllem2  47852  vonioo  47907  vonicc  47910  pimincfltioc  47941  smflimlem3  47998  smflimlem4  47999