Theorem chvarfv 2248

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2400 with a disjoint variable condition, which does not require ax-13 2377. (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  3866  axrep2  5215  axrep3  5216  isso2i  5569  frpoinsg  6301  tfindes  7807  findes  7844  dfoprab4f  8002  dom2lem  8932  setinds  9661  frinsg  9666  pwfseqlem4a  10575  pwfseqlem4  10576  uzind4s  12849  seqof2  14013  fsumclf  15691  fsumsplitf  15695  fproddivf  15943  fprodsplitf  15944  gsumcom2  19941  mdetralt2  22584  mdetunilem2  22588  ptcldmpt  23589  elmptrab  23802  isfildlem  23832  dvmptfsum  25952  dvfsumlem2  26004  lgamgulmlem2  27007  fmptcof2  32745  aciunf1lem  32750  fsumiunle  32917  esum2dlem  34252  fiunelros  34334  measiun  34378  bnj849  35083  bnj1014  35119  bnj1384  35190  bnj1489  35214  bnj1497  35218  finxpreclem6  37726  ptrest  37954  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  fdc1  38081  fsumshftd  39412  fphpd  43262  monotuz  43387  monotoddzz  43389  oddcomabszz  43390  setindtrs  43471  flcidc  43616  binomcxplemnotnn0  44801  fiiuncl  45514  disjf1  45631  disjinfi  45640  supxrleubrnmptf  45897  monoordxr  45928  monoord2xr  45930  fsummulc1f  46019  fsumnncl  46020  fsumf1of  46022  fsumiunss  46023  fsumreclf  46024  fsumlessf  46025  fsumsermpt  46027  fmul01  46028  fmuldfeq  46031  fmul01lt1lem1  46032  fmul01lt1lem2  46033  fprodexp  46042  fprodabs2  46043  climmulf  46052  climexp  46053  climsuse  46056  climrecf  46057  climinff  46059  climaddf  46063  mullimc  46064  neglimc  46093  addlimc  46094  0ellimcdiv  46095  climsubmpt  46106  climreclf  46110  climeldmeqmpt  46114  climfveqmpt  46117  fnlimfvre  46120  climfveqf  46126  climfveqmpt3  46128  climeldmeqf  46129  climeqf  46134  climeldmeqmpt3  46135  climinf2  46153  climinf2mpt  46160  climinfmpt  46161  limsupequz  46169  limsupequzmptf  46177  fprodcncf  46346  dvmptmulf  46383  dvnmptdivc  46384  dvnmul  46389  dvmptfprod  46391  stoweidlem3  46449  stoweidlem34  46480  stoweidlem42  46488  stoweidlem48  46494  fourierdlem112  46664  sge0lempt  46856  sge0iunmptlemfi  46859  sge0iunmptlemre  46861  sge0iunmpt  46864  sge0ltfirpmpt2  46872  sge0isummpt2  46878  sge0xaddlem2  46880  sge0xadd  46881  meadjiun  46912  voliunsge0lem  46918  meaiunincf  46929  meaiuninc3  46931  meaiininc  46933  hoimbl2  47111  vonhoire  47118  vonn0ioo2  47136  vonn0icc2  47138  salpreimagtlt  47176