Theorem chvarvv 1989

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2395 with a disjoint variable condition, which does not require ax-13 2371. (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  2704  axrep1  5238  axsepg  5255  tz6.12f  6887  frrlem12  8279  dfac12lem2  10105  wunex2  10698  ltordlem  11710  prodfdiv  15869  iscatd2  17649  yoniso  18253  mndind  18762  gsum2dlem2  19908  isdrngrd  20682  isdrngrdOLD  20684  frlmphl  21697  frlmup1  21714  mdetralt  22502  mdetunilem9  22514  neiptoptop  23025  neiptopnei  23026  cnextcn  23961  cnextfres1  23962  ustuqtop4  24139  dscmet  24467  nrmmetd  24469  rolle  25901  numclwlk2lem2f1o  30315  chscllem2  31574  suppovss  32611  fedgmullem1  33632  esumcvg  34083  eulerpartlemgvv  34374  eulerpartlemn  34379  bnj1326  35023  fwddifnp1  36160  poimirlem13  37634  poimirlem14  37635  poimirlem25  37646  poimirlem31  37652  ftc1anclem7  37700  ftc1anc  37702  fdc  37746  fdc1  37747  iscringd  37999  sticksstones2  42142  ismrcd2  42694  fphpdo  42812  monotoddzzfi  42938  monotoddzz  42939  mendlmod  43185  dvgrat  44308  cvgdvgrat  44309  binomcxplemnotnn0  44352  iunincfi  45095  wessf1ornlem  45186  monoords  45302  limcperiod  45633  sumnnodd  45635  cncfshift  45879  cncfperiod  45884  icccncfext  45892  fperdvper  45924  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  iblspltprt  45978  itgspltprt  45984  stoweidlem43  46048  stoweidlem62  46067  dirkercncflem2  46109  fourierdlem12  46124  fourierdlem15  46127  fourierdlem34  46146  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem50  46161  fourierdlem51  46162  fourierdlem73  46184  fourierdlem79  46190  fourierdlem81  46192  fourierdlem83  46194  fourierdlem92  46203  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  etransclem2  46241  etransclem46  46285  intsaluni  46334  meaiuninclem  46485  meaiuninc3v  46489  meaiininclem  46491  ovn0lem  46570  hoidmvlelem2  46601  hoidmvlelem3  46602  hspmbllem2  46632  vonioo  46687  vonicc  46690  pimincfltioc  46721  smflimlem3  46778  smflimlem4  46779