Theorem chvarvv 2022

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2431 with a disjoint variable condition, which does not require ax-13 2407. (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 2021	. 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 1943  ax-6 2000

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

This theorem is used by:  axextg  2740  axrep1  5244  axsepg  5263  tz6.12f  6913  frrlem12  8303  dfac12lem2  10147  wunex2  10741  ltordlem  11757  prodfdiv  15976  iscatd2  17762  yoniso  18366  mndind  18918  gsum2dlem2  20072  isdrngrd  20906  isdrngrdOLD  20908  frlmphl  21968  frlmup1  21985  mdetralt  22802  mdetunilem9  22814  neiptoptop  23325  neiptopnei  23326  cnextcn  24261  cnextfres1  24262  ustuqtop4  24438  dscmet  24766  nrmmetd  24768  rolle  26186  numclwlk2lem2f1o  30767  chscllem2  32027  suppovss  33063  fedgmullem1  34050  esumcvg  34507  eulerpartlemgvv  34798  eulerpartlemn  34803  bnj1326  35446  fwddifnp1  36678  axtco1  37025  axtco1from2  37027  poimirlem13  38325  poimirlem14  38326  poimirlem25  38337  poimirlem31  38343  ftc1anclem7  38391  ftc1anc  38393  fdc  38437  fdc1  38438  iscringd  38690  sticksstones2  42955  ismrcd2  43471  fphpdo  43585  monotoddzzfi  43710  monotoddzz  43711  mendlmod  43957  dvgrat  45063  cvgdvgrat  45064  binomcxplemnotnn0  45107  iunincfi  45853  wessf1ornlem  45944  monoords  46057  limcperiod  46385  sumnnodd  46387  cncfshift  46629  cncfperiod  46634  icccncfext  46642  fperdvper  46674  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  iblspltprt  46728  itgspltprt  46734  stoweidlem43  46798  stoweidlem62  46817  dirkercncflem2  46859  fourierdlem12  46874  fourierdlem15  46877  fourierdlem34  46896  fourierdlem41  46903  fourierdlem42  46904  fourierdlem48  46909  fourierdlem50  46911  fourierdlem51  46912  fourierdlem73  46934  fourierdlem79  46940  fourierdlem81  46942  fourierdlem83  46944  fourierdlem92  46953  fourierdlem94  46955  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  etransclem2  46991  etransclem46  47035  intsaluni  47084  meaiuninclem  47235  meaiuninc3v  47239  meaiininclem  47241  ovn0lem  47320  hoidmvlelem2  47351  hoidmvlelem3  47352  hspmbllem2  47382  vonioo  47437  vonicc  47440  pimincfltioc  47471  smflimlem3  47528  smflimlem4  47529