Theorem chvarvv 1990

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2398 with a disjoint variable condition, which does not require ax-13 2374. (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  2707  axrep1  5220  axsepg  5237  tz6.12f  6853  frrlem12  8233  dfac12lem2  10043  wunex2  10636  ltordlem  11649  prodfdiv  15805  iscatd2  17589  yoniso  18193  mndind  18738  gsum2dlem2  19885  isdrngrd  20683  isdrngrdOLD  20685  frlmphl  21720  frlmup1  21737  mdetralt  22524  mdetunilem9  22536  neiptoptop  23047  neiptopnei  23048  cnextcn  23983  cnextfres1  23984  ustuqtop4  24160  dscmet  24488  nrmmetd  24490  rolle  25922  numclwlk2lem2f1o  30361  chscllem2  31620  suppovss  32666  fedgmullem1  33663  esumcvg  34120  eulerpartlemgvv  34410  eulerpartlemn  34415  bnj1326  35059  fwddifnp1  36230  poimirlem13  37693  poimirlem14  37694  poimirlem25  37705  poimirlem31  37711  ftc1anclem7  37759  ftc1anc  37761  fdc  37805  fdc1  37806  iscringd  38058  sticksstones2  42260  ismrcd2  42816  fphpdo  42934  monotoddzzfi  43059  monotoddzz  43060  mendlmod  43306  dvgrat  44429  cvgdvgrat  44430  binomcxplemnotnn0  44473  iunincfi  45215  wessf1ornlem  45306  monoords  45422  limcperiod  45752  sumnnodd  45754  cncfshift  45996  cncfperiod  46001  icccncfext  46009  fperdvper  46041  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  iblspltprt  46095  itgspltprt  46101  stoweidlem43  46165  stoweidlem62  46184  dirkercncflem2  46226  fourierdlem12  46241  fourierdlem15  46244  fourierdlem34  46263  fourierdlem41  46270  fourierdlem42  46271  fourierdlem48  46276  fourierdlem50  46278  fourierdlem51  46279  fourierdlem73  46301  fourierdlem79  46307  fourierdlem81  46309  fourierdlem83  46311  fourierdlem92  46320  fourierdlem94  46322  fourierdlem103  46331  fourierdlem104  46332  fourierdlem111  46339  fourierdlem112  46340  fourierdlem113  46341  etransclem2  46358  etransclem46  46402  intsaluni  46451  meaiuninclem  46602  meaiuninc3v  46606  meaiininclem  46608  ovn0lem  46687  hoidmvlelem2  46718  hoidmvlelem3  46719  hspmbllem2  46749  vonioo  46804  vonicc  46807  pimincfltioc  46838  smflimlem3  46895  smflimlem4  46896