Theorem chvarvv 1996

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2404 with a disjoint variable condition, which does not require ax-13 2380. (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 1995	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1804	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  axextg  2714  axrep1  5207  axsepg  5226  tz6.12f  6859  frrlem12  8244  dfac12lem2  10065  wunex2  10659  ltordlem  11673  prodfdiv  15859  iscatd2  17645  yoniso  18249  mndind  18794  gsum2dlem2  19944  isdrngrd  20745  isdrngrdOLD  20747  frlmphl  21763  frlmup1  21780  mdetralt  22598  mdetunilem9  22610  neiptoptop  23121  neiptopnei  23122  cnextcn  24057  cnextfres1  24058  ustuqtop4  24234  dscmet  24562  nrmmetd  24564  rolle  25982  numclwlk2lem2f1o  30474  chscllem2  31734  suppovss  32780  fedgmullem1  33820  esumcvg  34277  eulerpartlemgvv  34567  eulerpartlemn  34572  bnj1326  35215  fwddifnp1  36400  axtco1  36708  axtco1from2  36710  poimirlem13  38007  poimirlem14  38008  poimirlem25  38019  poimirlem31  38025  ftc1anclem7  38073  ftc1anc  38075  fdc  38119  fdc1  38120  iscringd  38372  sticksstones2  42639  ismrcd2  43155  fphpdo  43269  monotoddzzfi  43394  monotoddzz  43395  mendlmod  43641  dvgrat  44763  cvgdvgrat  44764  binomcxplemnotnn0  44807  iunincfi  45548  wessf1ornlem  45639  monoords  45752  limcperiod  46080  sumnnodd  46082  cncfshift  46324  cncfperiod  46329  icccncfext  46337  fperdvper  46369  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  iblspltprt  46423  itgspltprt  46429  stoweidlem43  46493  stoweidlem62  46512  dirkercncflem2  46554  fourierdlem12  46569  fourierdlem15  46572  fourierdlem34  46591  fourierdlem41  46598  fourierdlem42  46599  fourierdlem48  46604  fourierdlem50  46606  fourierdlem51  46607  fourierdlem73  46629  fourierdlem79  46635  fourierdlem81  46637  fourierdlem83  46639  fourierdlem92  46648  fourierdlem94  46650  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  etransclem2  46686  etransclem46  46730  intsaluni  46779  meaiuninclem  46930  meaiuninc3v  46934  meaiininclem  46936  ovn0lem  47015  hoidmvlelem2  47046  hoidmvlelem3  47047  hspmbllem2  47077  vonioo  47132  vonicc  47135  pimincfltioc  47166  smflimlem3  47223  smflimlem4  47224