Theorem chvarvv 1990

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2400 with a disjoint variable condition, which does not require ax-13 2376. (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 1989	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1798	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 1796  ax-4 1810  ax-5 1911  ax-6 1968

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

This theorem is referenced by:  axextg  2710  axrep1  5225  axsepg  5242  tz6.12f  6859  frrlem12  8239  dfac12lem2  10055  wunex2  10649  ltordlem  11662  prodfdiv  15819  iscatd2  17604  yoniso  18208  mndind  18753  gsum2dlem2  19900  isdrngrd  20699  isdrngrdOLD  20701  frlmphl  21736  frlmup1  21753  mdetralt  22552  mdetunilem9  22564  neiptoptop  23075  neiptopnei  23076  cnextcn  24011  cnextfres1  24012  ustuqtop4  24188  dscmet  24516  nrmmetd  24518  rolle  25950  numclwlk2lem2f1o  30454  chscllem2  31713  suppovss  32760  fedgmullem1  33786  esumcvg  34243  eulerpartlemgvv  34533  eulerpartlemn  34538  bnj1326  35182  fwddifnp1  36359  poimirlem13  37830  poimirlem14  37831  poimirlem25  37842  poimirlem31  37848  ftc1anclem7  37896  ftc1anc  37898  fdc  37942  fdc1  37943  iscringd  38195  sticksstones2  42397  ismrcd2  42937  fphpdo  43055  monotoddzzfi  43180  monotoddzz  43181  mendlmod  43427  dvgrat  44549  cvgdvgrat  44550  binomcxplemnotnn0  44593  iunincfi  45334  wessf1ornlem  45425  monoords  45541  limcperiod  45870  sumnnodd  45872  cncfshift  46114  cncfperiod  46119  icccncfext  46127  fperdvper  46159  dvnprodlem1  46186  dvnprodlem2  46187  dvnprodlem3  46188  iblspltprt  46213  itgspltprt  46219  stoweidlem43  46283  stoweidlem62  46302  dirkercncflem2  46344  fourierdlem12  46359  fourierdlem15  46362  fourierdlem34  46381  fourierdlem41  46388  fourierdlem42  46389  fourierdlem48  46394  fourierdlem50  46396  fourierdlem51  46397  fourierdlem73  46419  fourierdlem79  46425  fourierdlem81  46427  fourierdlem83  46429  fourierdlem92  46438  fourierdlem94  46440  fourierdlem103  46449  fourierdlem104  46450  fourierdlem111  46457  fourierdlem112  46458  fourierdlem113  46459  etransclem2  46476  etransclem46  46520  intsaluni  46569  meaiuninclem  46720  meaiuninc3v  46724  meaiininclem  46726  ovn0lem  46805  hoidmvlelem2  46836  hoidmvlelem3  46837  hspmbllem2  46867  vonioo  46922  vonicc  46925  pimincfltioc  46956  smflimlem3  47013  smflimlem4  47014