Theorem chvarfv 2248

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2399 with a disjoint variable condition, which does not require ax-13 2376. (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 229	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2247	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1799	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785

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 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  csbhypf  3865  axrep2  5215  axrep3  5216  isso2i  5576  frpoinsg  6307  tfindes  7814  findes  7851  dfoprab4f  8009  dom2lem  8939  setinds  9670  frinsg  9675  pwfseqlem4a  10584  pwfseqlem4  10585  uzind4s  12858  seqof2  14022  fsumclf  15700  fsumsplitf  15704  fproddivf  15952  fprodsplitf  15953  gsumcom2  19950  mdetralt2  22574  mdetunilem2  22578  ptcldmpt  23579  elmptrab  23792  isfildlem  23822  dvmptfsum  25942  dvfsumlem2  25994  lgamgulmlem2  26993  fmptcof2  32730  aciunf1lem  32735  fsumiunle  32902  esum2dlem  34236  fiunelros  34318  measiun  34362  bnj849  35067  bnj1014  35103  bnj1384  35174  bnj1489  35198  bnj1497  35202  finxpreclem6  37712  ptrest  37940  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  fdc1  38067  fsumshftd  39398  fphpd  43244  monotuz  43369  monotoddzz  43371  oddcomabszz  43372  setindtrs  43453  flcidc  43598  binomcxplemnotnn0  44783  fiiuncl  45496  disjf1  45613  disjinfi  45622  supxrleubrnmptf  45879  monoordxr  45910  monoord2xr  45912  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmul01  46010  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fprodexp  46024  fprodabs2  46025  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  neglimc  46075  addlimc  46076  0ellimcdiv  46077  climsubmpt  46088  climreclf  46092  climeldmeqmpt  46096  climfveqmpt  46099  fnlimfvre  46102  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  climeqf  46116  climeldmeqmpt3  46117  climinf2  46135  climinf2mpt  46142  climinfmpt  46143  limsupequz  46151  limsupequzmptf  46159  fprodcncf  46328  dvmptmulf  46365  dvnmptdivc  46366  dvnmul  46371  dvmptfprod  46373  stoweidlem3  46431  stoweidlem34  46462  stoweidlem42  46470  stoweidlem48  46476  fourierdlem112  46646  sge0lempt  46838  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  meadjiun  46894  voliunsge0lem  46900  meaiunincf  46911  meaiuninc3  46913  meaiininc  46915  hoimbl2  47093  vonhoire  47100  vonn0ioo2  47118  vonn0icc2  47120  salpreimagtlt  47158