Theorem chvarfv 2240

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 2239	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1797	1 ⊢ 𝜓

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  csbhypf  3927  axrep2  5282  axrep3  5283  isso2i  5629  frpoinsg  6364  wfisgOLD  6375  tfindes  7884  findes  7922  dfoprab4f  8081  dom2lem  9032  frinsg  9791  pwfseqlem4a  10701  pwfseqlem4  10702  uzind4s  12950  seqof2  14101  fsumclf  15774  fsumsplitf  15778  fproddivf  16023  fprodsplitf  16024  gsumcom2  19993  mdetralt2  22615  mdetunilem2  22619  ptcldmpt  23622  elmptrab  23835  isfildlem  23865  dvmptfsum  26013  dvfsumlem2  26067  dvfsumlem2OLD  26068  lgamgulmlem2  27073  fmptcof2  32667  aciunf1lem  32672  fsumiunle  32831  esum2dlem  34093  fiunelros  34175  measiun  34219  bnj849  34939  bnj1014  34975  bnj1384  35046  bnj1489  35070  bnj1497  35074  setinds  35779  finxpreclem6  37397  ptrest  37626  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  fdc1  37753  fsumshftd  38953  fphpd  42827  monotuz  42953  monotoddzz  42955  oddcomabszz  42956  setindtrs  43037  flcidc  43182  binomcxplemnotnn0  44375  fiiuncl  45070  disjf1  45188  disjinfi  45197  supxrleubrnmptf  45462  monoordxr  45493  monoord2xr  45495  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumiunss  45590  fsumreclf  45591  fsumlessf  45592  fsumsermpt  45594  fmul01  45595  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fprodexp  45609  fprodabs2  45610  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climinff  45626  climaddf  45630  mullimc  45631  neglimc  45662  addlimc  45663  0ellimcdiv  45664  climsubmpt  45675  climreclf  45679  climeldmeqmpt  45683  climfveqmpt  45686  fnlimfvre  45689  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  climeqf  45703  climeldmeqmpt3  45704  climinf2  45722  climinf2mpt  45729  climinfmpt  45730  limsupequz  45738  limsupequzmptf  45746  fprodcncf  45915  dvmptmulf  45952  dvnmptdivc  45953  dvnmul  45958  dvmptfprod  45960  stoweidlem3  46018  stoweidlem34  46049  stoweidlem42  46057  stoweidlem48  46063  fourierdlem112  46233  sge0lempt  46425  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  meadjiun  46481  voliunsge0lem  46487  meaiunincf  46498  meaiuninc3  46500  meaiininc  46502  hoimbl2  46680  vonhoire  46687  vonn0ioo2  46705  vonn0icc2  46707  salpreimagtlt  46745