Theorem chvarvv 1998

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 1996	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1797	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 1795  ax-4 1809  ax-5 1910  ax-6 1967

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

This theorem is referenced by:  axextg  2709  axrep1  5250  axsepg  5267  tz6.12f  6902  frrlem12  8296  dfac12lem2  10159  wunex2  10752  ltordlem  11762  prodfdiv  15912  iscatd2  17693  yoniso  18297  mndind  18806  gsum2dlem2  19952  isdrngrd  20726  isdrngrdOLD  20728  frlmphl  21741  frlmup1  21758  mdetralt  22546  mdetunilem9  22558  neiptoptop  23069  neiptopnei  23070  cnextcn  24005  cnextfres1  24006  ustuqtop4  24183  dscmet  24511  nrmmetd  24513  rolle  25946  numclwlk2lem2f1o  30360  chscllem2  31619  suppovss  32658  fedgmullem1  33669  esumcvg  34117  eulerpartlemgvv  34408  eulerpartlemn  34413  bnj1326  35057  fwddifnp1  36183  poimirlem13  37657  poimirlem14  37658  poimirlem25  37669  poimirlem31  37675  ftc1anclem7  37723  ftc1anc  37725  fdc  37769  fdc1  37770  iscringd  38022  sticksstones2  42160  ismrcd2  42722  fphpdo  42840  monotoddzzfi  42966  monotoddzz  42967  mendlmod  43213  dvgrat  44336  cvgdvgrat  44337  binomcxplemnotnn0  44380  iunincfi  45118  wessf1ornlem  45209  monoords  45326  limcperiod  45657  sumnnodd  45659  cncfshift  45903  cncfperiod  45908  icccncfext  45916  fperdvper  45948  dvnprodlem1  45975  dvnprodlem2  45976  dvnprodlem3  45977  iblspltprt  46002  itgspltprt  46008  stoweidlem43  46072  stoweidlem62  46091  dirkercncflem2  46133  fourierdlem12  46148  fourierdlem15  46151  fourierdlem34  46170  fourierdlem41  46177  fourierdlem42  46178  fourierdlem48  46183  fourierdlem50  46185  fourierdlem51  46186  fourierdlem73  46208  fourierdlem79  46214  fourierdlem81  46216  fourierdlem83  46218  fourierdlem92  46227  fourierdlem94  46229  fourierdlem103  46238  fourierdlem104  46239  fourierdlem111  46246  fourierdlem112  46247  fourierdlem113  46248  etransclem2  46265  etransclem46  46309  intsaluni  46358  meaiuninclem  46509  meaiuninc3v  46513  meaiininclem  46515  ovn0lem  46594  hoidmvlelem2  46625  hoidmvlelem3  46626  hspmbllem2  46656  vonioo  46711  vonicc  46714  pimincfltioc  46745  smflimlem3  46802  smflimlem4  46803