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  5219  axsepg  5236  tz6.12f  6847  frrlem12  8230  dfac12lem2  10039  wunex2  10632  ltordlem  11645  prodfdiv  15803  iscatd2  17587  yoniso  18191  mndind  18702  gsum2dlem2  19850  isdrngrd  20651  isdrngrdOLD  20653  frlmphl  21688  frlmup1  21705  mdetralt  22493  mdetunilem9  22505  neiptoptop  23016  neiptopnei  23017  cnextcn  23952  cnextfres1  23953  ustuqtop4  24130  dscmet  24458  nrmmetd  24460  rolle  25892  numclwlk2lem2f1o  30323  chscllem2  31582  suppovss  32624  fedgmullem1  33602  esumcvg  34059  eulerpartlemgvv  34350  eulerpartlemn  34355  bnj1326  34999  fwddifnp1  36149  poimirlem13  37623  poimirlem14  37624  poimirlem25  37635  poimirlem31  37641  ftc1anclem7  37689  ftc1anc  37691  fdc  37735  fdc1  37736  iscringd  37988  sticksstones2  42130  ismrcd2  42682  fphpdo  42800  monotoddzzfi  42925  monotoddzz  42926  mendlmod  43172  dvgrat  44295  cvgdvgrat  44296  binomcxplemnotnn0  44339  iunincfi  45082  wessf1ornlem  45173  monoords  45289  limcperiod  45619  sumnnodd  45621  cncfshift  45865  cncfperiod  45870  icccncfext  45878  fperdvper  45910  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  iblspltprt  45964  itgspltprt  45970  stoweidlem43  46034  stoweidlem62  46053  dirkercncflem2  46095  fourierdlem12  46110  fourierdlem15  46113  fourierdlem34  46132  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem50  46147  fourierdlem51  46148  fourierdlem73  46170  fourierdlem79  46176  fourierdlem81  46178  fourierdlem83  46180  fourierdlem92  46189  fourierdlem94  46191  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  etransclem2  46227  etransclem46  46271  intsaluni  46320  meaiuninclem  46471  meaiuninc3v  46475  meaiininclem  46477  ovn0lem  46556  hoidmvlelem2  46587  hoidmvlelem3  46588  hspmbllem2  46618  vonioo  46673  vonicc  46676  pimincfltioc  46707  smflimlem3  46764  smflimlem4  46765