Theorem chvarvv 1995

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2391 with a disjoint variable condition, which does not require ax-13 2367. (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 1993	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
3		chvarvv.2	. 2 ⊢ 𝜑
4	2, 3	mpg 1792	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 1790  ax-4 1804  ax-5 1906  ax-6 1964

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

This theorem is referenced by:  axextg  2701  nfcriOLD  2889  nfcriOLDOLD  2890  axrep1  5281  axsepg  5295  tz6.12f  6918  frrlem12  8297  dfac12lem2  10162  wunex2  10756  ltordlem  11764  prodfdiv  15869  iscatd2  17655  yoniso  18271  mndind  18774  gsum2dlem2  19920  isdrngrd  20652  isdrngrdOLD  20654  frlmphl  21709  frlmup1  21726  mdetralt  22504  mdetunilem9  22516  neiptoptop  23029  neiptopnei  23030  cnextcn  23965  cnextfres1  23966  ustuqtop4  24143  dscmet  24475  nrmmetd  24477  rolle  25916  numclwlk2lem2f1o  30183  chscllem2  31442  suppovss  32459  fedgmullem1  33318  esumcvg  33700  eulerpartlemgvv  33991  eulerpartlemn  33996  bnj1326  34652  fwddifnp1  35756  poimirlem13  37101  poimirlem14  37102  poimirlem25  37113  poimirlem31  37119  ftc1anclem7  37167  ftc1anc  37169  fdc  37213  fdc1  37214  iscringd  37466  sticksstones2  41614  ismrcd2  42110  fphpdo  42228  monotoddzzfi  42354  monotoddzz  42355  mendlmod  42608  dvgrat  43740  cvgdvgrat  43741  binomcxplemnotnn0  43784  iunincfi  44451  wessf1ornlem  44549  monoords  44670  limcperiod  45007  sumnnodd  45009  cncfshift  45253  cncfperiod  45258  icccncfext  45266  fperdvper  45298  dvnprodlem1  45325  dvnprodlem2  45326  dvnprodlem3  45327  iblspltprt  45352  itgspltprt  45358  stoweidlem43  45422  stoweidlem62  45441  dirkercncflem2  45483  fourierdlem12  45498  fourierdlem15  45501  fourierdlem34  45520  fourierdlem41  45527  fourierdlem42  45528  fourierdlem48  45533  fourierdlem50  45535  fourierdlem51  45536  fourierdlem73  45558  fourierdlem79  45564  fourierdlem81  45566  fourierdlem83  45568  fourierdlem92  45577  fourierdlem94  45579  fourierdlem103  45588  fourierdlem104  45589  fourierdlem111  45596  fourierdlem112  45597  fourierdlem113  45598  etransclem2  45615  etransclem46  45659  intsaluni  45708  meaiuninclem  45859  meaiuninc3v  45863  meaiininclem  45865  ovn0lem  45944  hoidmvlelem2  45975  hoidmvlelem3  45976  hspmbllem2  46006  vonioo  46061  vonicc  46064  pimincfltioc  46095  smflimlem3  46152  smflimlem4  46153