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  5235  axsepg  5252  tz6.12f  6884  frrlem12  8276  dfac12lem2  10098  wunex2  10691  ltordlem  11703  prodfdiv  15862  iscatd2  17642  yoniso  18246  mndind  18755  gsum2dlem2  19901  isdrngrd  20675  isdrngrdOLD  20677  frlmphl  21690  frlmup1  21707  mdetralt  22495  mdetunilem9  22507  neiptoptop  23018  neiptopnei  23019  cnextcn  23954  cnextfres1  23955  ustuqtop4  24132  dscmet  24460  nrmmetd  24462  rolle  25894  numclwlk2lem2f1o  30308  chscllem2  31567  suppovss  32604  fedgmullem1  33625  esumcvg  34076  eulerpartlemgvv  34367  eulerpartlemn  34372  bnj1326  35016  fwddifnp1  36153  poimirlem13  37627  poimirlem14  37628  poimirlem25  37639  poimirlem31  37645  ftc1anclem7  37693  ftc1anc  37695  fdc  37739  fdc1  37740  iscringd  37992  sticksstones2  42135  ismrcd2  42687  fphpdo  42805  monotoddzzfi  42931  monotoddzz  42932  mendlmod  43178  dvgrat  44301  cvgdvgrat  44302  binomcxplemnotnn0  44345  iunincfi  45088  wessf1ornlem  45179  monoords  45295  limcperiod  45626  sumnnodd  45628  cncfshift  45872  cncfperiod  45877  icccncfext  45885  fperdvper  45917  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  iblspltprt  45971  itgspltprt  45977  stoweidlem43  46041  stoweidlem62  46060  dirkercncflem2  46102  fourierdlem12  46117  fourierdlem15  46120  fourierdlem34  46139  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem50  46154  fourierdlem51  46155  fourierdlem73  46177  fourierdlem79  46183  fourierdlem81  46185  fourierdlem83  46187  fourierdlem92  46196  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  etransclem2  46234  etransclem46  46278  intsaluni  46327  meaiuninclem  46478  meaiuninc3v  46482  meaiininclem  46484  ovn0lem  46563  hoidmvlelem2  46594  hoidmvlelem3  46595  hspmbllem2  46625  vonioo  46680  vonicc  46683  pimincfltioc  46714  smflimlem3  46771  smflimlem4  46772