Theorem chvarfv 2277

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2425 with a disjoint variable condition, which does not require ax-13 2402. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.)

Hypotheses

Ref	Expression
chvarfv.nf	⊢ Ⅎ𝑥𝜓
chvarfv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvarfv.2	⊢ 𝜑

Assertion

Ref	Expression
chvarfv	⊢ 𝜓

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑥, 𝑦)

Proof of Theorem chvarfv

Step	Hyp	Ref	Expression
1		chvarfv.nf	. . 3 ⊢ Ⅎ𝑥𝜓
2		chvarfv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpd 232	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2276	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1830	1 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  csbhypf  3875  axrep2  5235  axrep3  5236  isso2i  5596  frpoinsg  6345  tfindes  7872  findes  7910  dfoprab4f  8065  dom2lem  9012  setinds  9743  frinsg  9748  pwfseqlem4a  10739  pwfseqlem4  10740  uzind4s  13028  seqof2  14196  fsumclf  15897  fsumsplitf  15901  fproddivf  16147  fprodsplitf  16148  gsumcom2  20182  mdetralt2  22917  mdetunilem2  22921  ptcldmpt  23926  elmptrab  24139  isfildlem  24169  dvmptfsum  26288  dvfsumlem2  26340  lgamgulmlem2  27350  fmptcof2  33244  aciunf1lem  33249  fsumiunle  33413  esum2dlem  34717  fiunelros  34800  measiun  34844  bnj849  35548  bnj1014  35584  bnj1384  35655  bnj1489  35679  bnj1497  35683  finxpreclem6  38299  ptrest  38517  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  fdc1  38660  fsumshftd  39989  fphpd  43802  monotuz  43927  monotoddzz  43929  oddcomabszz  43930  setindtrs  44011  flcidc  44156  binomcxplemnotnn0  45325  fiiuncl  46051  disjf1  46167  disjinfi  46176  supxrleubrnmptf  46430  monoordxr  46461  monoord2xr  46463  fsummulc1f  46552  fsumnncl  46553  fsumf1of  46555  fsumiunss  46556  fsumreclf  46557  fsumlessf  46558  fsumsermpt  46560  fmul01  46561  fmuldfeq  46564  fmul01lt1lem1  46565  fmul01lt1lem2  46566  fprodexp  46575  fprodabs2  46576  climmulf  46585  climexp  46586  climsuse  46589  climrecf  46590  climinff  46592  climaddf  46596  mullimc  46597  neglimc  46626  addlimc  46627  0ellimcdiv  46628  climsubmpt  46639  climreclf  46643  climeldmeqmpt  46647  climfveqmpt  46650  fnlimfvre  46653  climfveqf  46659  climfveqmpt3  46661  climeldmeqf  46662  climeqf  46667  climeldmeqmpt3  46668  climinf2  46686  climinf2mpt  46693  climinfmpt  46694  limsupequz  46702  limsupequzmptf  46710  fprodcncf  46879  dvmptmulf  46916  dvnmptdivc  46917  dvnmul  46922  dvmptfprod  46924  stoweidlem3  46982  stoweidlem34  47013  stoweidlem42  47021  stoweidlem48  47027  fourierdlem112  47197  sge0lempt  47389  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  sge0ltfirpmpt2  47405  sge0isummpt2  47411  sge0xaddlem2  47413  sge0xadd  47414  meadjiun  47445  voliunsge0lem  47451  meaiunincf  47462  meaiuninc3  47464  meaiininc  47466  hoimbl2  47644  vonhoire  47651  vonn0ioo2  47669  vonn0icc2  47671  salpreimagtlt  47709