Theorem chvarvv 2005

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  axextg  2772  nfcriOLD  2946  nfcriOLDOLD  2947  axrep1  5155  axsepg  5168  tz6.12f  6669  dfac12lem2  9555  wunex2  10149  ltordlem  11154  prodfdiv  15244  iscatd2  16944  yoniso  17527  mndind  17984  gsum2dlem2  19084  isdrngrd  19521  frlmphl  20470  frlmup1  20487  mdetralt  21213  mdetunilem9  21225  neiptoptop  21736  neiptopnei  21737  cnextcn  22672  cnextfres1  22673  ustuqtop4  22850  dscmet  23179  nrmmetd  23181  rolle  24593  numclwlk2lem2f1o  28164  chscllem2  29421  suppovss  30443  fedgmullem1  31113  esumcvg  31455  eulerpartlemgvv  31744  eulerpartlemn  31749  bnj1326  32408  frrlem12  33247  fwddifnp1  33739  poimirlem13  35070  poimirlem14  35071  poimirlem25  35082  poimirlem31  35088  ftc1anclem7  35136  ftc1anc  35138  fdc  35183  fdc1  35184  iscringd  35436  ismrcd2  39640  fphpdo  39758  monotoddzzfi  39883  monotoddzz  39884  mendlmod  40137  dvgrat  41016  cvgdvgrat  41017  binomcxplemnotnn0  41060  iunincfi  41730  wessf1ornlem  41811  monoords  41929  limcperiod  42270  sumnnodd  42272  cncfshift  42516  cncfperiod  42521  icccncfext  42529  fperdvper  42561  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  iblspltprt  42615  itgspltprt  42621  stoweidlem43  42685  stoweidlem62  42704  dirkercncflem2  42746  fourierdlem12  42761  fourierdlem15  42764  fourierdlem34  42783  fourierdlem41  42790  fourierdlem42  42791  fourierdlem48  42796  fourierdlem50  42798  fourierdlem51  42799  fourierdlem73  42821  fourierdlem79  42827  fourierdlem81  42829  fourierdlem83  42831  fourierdlem92  42840  fourierdlem94  42842  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  etransclem2  42878  etransclem46  42922  intsaluni  42969  meaiuninclem  43119  meaiuninc3v  43123  meaiininclem  43125  ovn0lem  43204  hoidmvlelem2  43235  hoidmvlelem3  43236  hspmbllem2  43266  vonioo  43321  vonicc  43324  pimincfltioc  43351  smflimlem3  43406  smflimlem4  43407