Theorem chvarvv 1989

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2394 with a disjoint variable condition, which does not require ax-13 2370. (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 1988	. 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  2703  axrep1  5222  axsepg  5239  tz6.12f  6851  frrlem12  8237  dfac12lem2  10058  wunex2  10651  ltordlem  11663  prodfdiv  15821  iscatd2  17605  yoniso  18209  mndind  18720  gsum2dlem2  19868  isdrngrd  20669  isdrngrdOLD  20671  frlmphl  21706  frlmup1  21723  mdetralt  22511  mdetunilem9  22523  neiptoptop  23034  neiptopnei  23035  cnextcn  23970  cnextfres1  23971  ustuqtop4  24148  dscmet  24476  nrmmetd  24478  rolle  25910  numclwlk2lem2f1o  30341  chscllem2  31600  suppovss  32637  fedgmullem1  33601  esumcvg  34052  eulerpartlemgvv  34343  eulerpartlemn  34348  bnj1326  34992  fwddifnp1  36138  poimirlem13  37612  poimirlem14  37613  poimirlem25  37624  poimirlem31  37630  ftc1anclem7  37678  ftc1anc  37680  fdc  37724  fdc1  37725  iscringd  37977  sticksstones2  42120  ismrcd2  42672  fphpdo  42790  monotoddzzfi  42915  monotoddzz  42916  mendlmod  43162  dvgrat  44285  cvgdvgrat  44286  binomcxplemnotnn0  44329  iunincfi  45072  wessf1ornlem  45163  monoords  45279  limcperiod  45610  sumnnodd  45612  cncfshift  45856  cncfperiod  45861  icccncfext  45869  fperdvper  45901  dvnprodlem1  45928  dvnprodlem2  45929  dvnprodlem3  45930  iblspltprt  45955  itgspltprt  45961  stoweidlem43  46025  stoweidlem62  46044  dirkercncflem2  46086  fourierdlem12  46101  fourierdlem15  46104  fourierdlem34  46123  fourierdlem41  46130  fourierdlem42  46131  fourierdlem48  46136  fourierdlem50  46138  fourierdlem51  46139  fourierdlem73  46161  fourierdlem79  46167  fourierdlem81  46169  fourierdlem83  46171  fourierdlem92  46180  fourierdlem94  46182  fourierdlem103  46191  fourierdlem104  46192  fourierdlem111  46199  fourierdlem112  46200  fourierdlem113  46201  etransclem2  46218  etransclem46  46262  intsaluni  46311  meaiuninclem  46462  meaiuninc3v  46466  meaiininclem  46468  ovn0lem  46547  hoidmvlelem2  46578  hoidmvlelem3  46579  hspmbllem2  46609  vonioo  46664  vonicc  46667  pimincfltioc  46698  smflimlem3  46755  smflimlem4  46756