Theorem chvarvv 1990

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 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  2705  axrep1  5218  axsepg  5235  tz6.12f  6847  frrlem12  8227  dfac12lem2  10033  wunex2  10626  ltordlem  11639  prodfdiv  15800  iscatd2  17584  yoniso  18188  mndind  18733  gsum2dlem2  19881  isdrngrd  20679  isdrngrdOLD  20681  frlmphl  21716  frlmup1  21733  mdetralt  22521  mdetunilem9  22533  neiptoptop  23044  neiptopnei  23045  cnextcn  23980  cnextfres1  23981  ustuqtop4  24157  dscmet  24485  nrmmetd  24487  rolle  25919  numclwlk2lem2f1o  30354  chscllem2  31613  suppovss  32657  fedgmullem1  33637  esumcvg  34094  eulerpartlemgvv  34384  eulerpartlemn  34389  bnj1326  35033  fwddifnp1  36198  poimirlem13  37672  poimirlem14  37673  poimirlem25  37684  poimirlem31  37690  ftc1anclem7  37738  ftc1anc  37740  fdc  37784  fdc1  37785  iscringd  38037  sticksstones2  42179  ismrcd2  42731  fphpdo  42849  monotoddzzfi  42974  monotoddzz  42975  mendlmod  43221  dvgrat  44344  cvgdvgrat  44345  binomcxplemnotnn0  44388  iunincfi  45130  wessf1ornlem  45221  monoords  45337  limcperiod  45667  sumnnodd  45669  cncfshift  45911  cncfperiod  45916  icccncfext  45924  fperdvper  45956  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  iblspltprt  46010  itgspltprt  46016  stoweidlem43  46080  stoweidlem62  46099  dirkercncflem2  46141  fourierdlem12  46156  fourierdlem15  46159  fourierdlem34  46178  fourierdlem41  46185  fourierdlem42  46186  fourierdlem48  46191  fourierdlem50  46193  fourierdlem51  46194  fourierdlem73  46216  fourierdlem79  46222  fourierdlem81  46224  fourierdlem83  46226  fourierdlem92  46235  fourierdlem94  46237  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem112  46255  fourierdlem113  46256  etransclem2  46273  etransclem46  46317  intsaluni  46366  meaiuninclem  46517  meaiuninc3v  46521  meaiininclem  46523  ovn0lem  46602  hoidmvlelem2  46633  hoidmvlelem3  46634  hspmbllem2  46664  vonioo  46719  vonicc  46722  pimincfltioc  46753  smflimlem3  46810  smflimlem4  46811