Theorem chvarvv 1998

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  axextg  2710  axrep1  5280  axsepg  5297  tz6.12f  6932  frrlem12  8322  dfac12lem2  10185  wunex2  10778  ltordlem  11788  prodfdiv  15932  iscatd2  17724  yoniso  18330  mndind  18841  gsum2dlem2  19989  isdrngrd  20766  isdrngrdOLD  20768  frlmphl  21801  frlmup1  21818  mdetralt  22614  mdetunilem9  22626  neiptoptop  23139  neiptopnei  23140  cnextcn  24075  cnextfres1  24076  ustuqtop4  24253  dscmet  24585  nrmmetd  24587  rolle  26028  numclwlk2lem2f1o  30398  chscllem2  31657  suppovss  32690  fedgmullem1  33680  esumcvg  34087  eulerpartlemgvv  34378  eulerpartlemn  34383  bnj1326  35040  fwddifnp1  36166  poimirlem13  37640  poimirlem14  37641  poimirlem25  37652  poimirlem31  37658  ftc1anclem7  37706  ftc1anc  37708  fdc  37752  fdc1  37753  iscringd  38005  sticksstones2  42148  ismrcd2  42710  fphpdo  42828  monotoddzzfi  42954  monotoddzz  42955  mendlmod  43201  dvgrat  44331  cvgdvgrat  44332  binomcxplemnotnn0  44375  iunincfi  45099  wessf1ornlem  45190  monoords  45309  limcperiod  45643  sumnnodd  45645  cncfshift  45889  cncfperiod  45894  icccncfext  45902  fperdvper  45934  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  iblspltprt  45988  itgspltprt  45994  stoweidlem43  46058  stoweidlem62  46077  dirkercncflem2  46119  fourierdlem12  46134  fourierdlem15  46137  fourierdlem34  46156  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem50  46171  fourierdlem51  46172  fourierdlem73  46194  fourierdlem79  46200  fourierdlem81  46202  fourierdlem83  46204  fourierdlem92  46213  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  etransclem2  46251  etransclem46  46295  intsaluni  46344  meaiuninclem  46495  meaiuninc3v  46499  meaiininclem  46501  ovn0lem  46580  hoidmvlelem2  46611  hoidmvlelem3  46612  hspmbllem2  46642  vonioo  46697  vonicc  46700  pimincfltioc  46731  smflimlem3  46788  smflimlem4  46789