Theorem chvarvv 2003

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  axextg  2711  nfcriOLD  2896  nfcriOLDOLD  2897  axrep1  5206  axsepg  5219  tz6.12f  6780  frrlem12  8084  dfac12lem2  9831  wunex2  10425  ltordlem  11430  prodfdiv  15536  iscatd2  17307  yoniso  17919  mndind  18381  gsum2dlem2  19487  isdrngrd  19932  frlmphl  20898  frlmup1  20915  mdetralt  21665  mdetunilem9  21677  neiptoptop  22190  neiptopnei  22191  cnextcn  23126  cnextfres1  23127  ustuqtop4  23304  dscmet  23634  nrmmetd  23636  rolle  25059  numclwlk2lem2f1o  28644  chscllem2  29901  suppovss  30919  fedgmullem1  31612  esumcvg  31954  eulerpartlemgvv  32243  eulerpartlemn  32248  bnj1326  32906  fwddifnp1  34394  poimirlem13  35717  poimirlem14  35718  poimirlem25  35729  poimirlem31  35735  ftc1anclem7  35783  ftc1anc  35785  fdc  35830  fdc1  35831  iscringd  36083  sticksstones2  40031  ismrcd2  40437  fphpdo  40555  monotoddzzfi  40680  monotoddzz  40681  mendlmod  40934  dvgrat  41819  cvgdvgrat  41820  binomcxplemnotnn0  41863  iunincfi  42533  wessf1ornlem  42611  monoords  42726  limcperiod  43059  sumnnodd  43061  cncfshift  43305  cncfperiod  43310  icccncfext  43318  fperdvper  43350  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  iblspltprt  43404  itgspltprt  43410  stoweidlem43  43474  stoweidlem62  43493  dirkercncflem2  43535  fourierdlem12  43550  fourierdlem15  43553  fourierdlem34  43572  fourierdlem41  43579  fourierdlem42  43580  fourierdlem48  43585  fourierdlem50  43587  fourierdlem51  43588  fourierdlem73  43610  fourierdlem79  43616  fourierdlem81  43618  fourierdlem83  43620  fourierdlem92  43629  fourierdlem94  43631  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  etransclem2  43667  etransclem46  43711  intsaluni  43758  meaiuninclem  43908  meaiuninc3v  43912  meaiininclem  43914  ovn0lem  43993  hoidmvlelem2  44024  hoidmvlelem3  44025  hspmbllem2  44055  vonioo  44110  vonicc  44113  pimincfltioc  44140  smflimlem3  44195  smflimlem4  44196