Theorem chvarvv 1991

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 1990	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1799	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 1797  ax-4 1811  ax-5 1912  ax-6 1969

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

This theorem is referenced by:  axextg  2711  axrep1  5213  axsepg  5232  tz6.12f  6859  frrlem12  8240  dfac12lem2  10058  wunex2  10652  ltordlem  11666  prodfdiv  15852  iscatd2  17638  yoniso  18242  mndind  18787  gsum2dlem2  19937  isdrngrd  20734  isdrngrdOLD  20736  frlmphl  21771  frlmup1  21788  mdetralt  22583  mdetunilem9  22595  neiptoptop  23106  neiptopnei  23107  cnextcn  24042  cnextfres1  24043  ustuqtop4  24219  dscmet  24547  nrmmetd  24549  rolle  25967  numclwlk2lem2f1o  30464  chscllem2  31724  suppovss  32769  fedgmullem1  33789  esumcvg  34246  eulerpartlemgvv  34536  eulerpartlemn  34541  bnj1326  35184  fwddifnp1  36363  axtco1  36671  axtco1from2  36673  poimirlem13  37968  poimirlem14  37969  poimirlem25  37980  poimirlem31  37986  ftc1anclem7  38034  ftc1anc  38036  fdc  38080  fdc1  38081  iscringd  38333  sticksstones2  42600  ismrcd2  43145  fphpdo  43263  monotoddzzfi  43388  monotoddzz  43389  mendlmod  43635  dvgrat  44757  cvgdvgrat  44758  binomcxplemnotnn0  44801  iunincfi  45542  wessf1ornlem  45633  monoords  45748  limcperiod  46076  sumnnodd  46078  cncfshift  46320  cncfperiod  46325  icccncfext  46333  fperdvper  46365  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  iblspltprt  46419  itgspltprt  46425  stoweidlem43  46489  stoweidlem62  46508  dirkercncflem2  46550  fourierdlem12  46565  fourierdlem15  46568  fourierdlem34  46587  fourierdlem41  46594  fourierdlem42  46595  fourierdlem48  46600  fourierdlem50  46602  fourierdlem51  46603  fourierdlem73  46625  fourierdlem79  46631  fourierdlem81  46633  fourierdlem83  46635  fourierdlem92  46644  fourierdlem94  46646  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  etransclem2  46682  etransclem46  46726  intsaluni  46775  meaiuninclem  46926  meaiuninc3v  46930  meaiininclem  46932  ovn0lem  47011  hoidmvlelem2  47042  hoidmvlelem3  47043  hspmbllem2  47073  vonioo  47128  vonicc  47131  pimincfltioc  47162  smflimlem3  47219  smflimlem4  47220