Theorem chvarfv 2231

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎ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 1911  ax-6 1969  ax-7 2009  ax-12 2169

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

This theorem is referenced by:  csbhypf  3921  axrep2  5287  axrep3  5288  isso2i  5622  frpoinsg  6343  wfisgOLD  6354  tfindes  7854  findes  7895  dfoprab4f  8044  dom2lem  8990  frinsg  9748  pwfseqlem4a  10658  pwfseqlem4  10659  uzind4s  12896  seqof2  14030  fsumclf  15688  fsumsplitf  15692  fproddivf  15935  fprodsplitf  15936  gsumcom2  19884  mdetralt2  22331  mdetunilem2  22335  ptcldmpt  23338  elmptrab  23551  isfildlem  23581  dvmptfsum  25727  dvfsumlem2  25779  lgamgulmlem2  26770  fmptcof2  32149  aciunf1lem  32154  fsumiunle  32302  esum2dlem  33388  fiunelros  33470  measiun  33514  bnj849  34234  bnj1014  34270  bnj1384  34341  bnj1489  34365  bnj1497  34369  setinds  35054  gg-dvfsumlem2  35469  finxpreclem6  36580  ptrest  36790  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  fdc1  36917  fsumshftd  38125  fphpd  41856  monotuz  41982  monotoddzz  41984  oddcomabszz  41985  setindtrs  42066  flcidc  42218  binomcxplemnotnn0  43417  fiiuncl  44053  disjf1  44180  disjinfi  44189  supxrleubrnmptf  44459  monoordxr  44491  monoord2xr  44493  fsummulc1f  44585  fsumnncl  44586  fsumf1of  44588  fsumiunss  44589  fsumreclf  44590  fsumlessf  44591  fsumsermpt  44593  fmul01  44594  fmuldfeq  44597  fmul01lt1lem1  44598  fmul01lt1lem2  44599  fprodexp  44608  fprodabs2  44609  climmulf  44618  climexp  44619  climsuse  44622  climrecf  44623  climinff  44625  climaddf  44629  mullimc  44630  neglimc  44661  addlimc  44662  0ellimcdiv  44663  climsubmpt  44674  climreclf  44678  climeldmeqmpt  44682  climfveqmpt  44685  fnlimfvre  44688  climfveqf  44694  climfveqmpt3  44696  climeldmeqf  44697  climeqf  44702  climeldmeqmpt3  44703  climinf2  44721  climinf2mpt  44728  climinfmpt  44729  limsupequz  44737  limsupequzmptf  44745  fprodcncf  44914  dvmptmulf  44951  dvnmptdivc  44952  dvnmul  44957  dvmptfprod  44959  stoweidlem3  45017  stoweidlem34  45048  stoweidlem42  45056  stoweidlem48  45062  fourierdlem112  45232  sge0lempt  45424  sge0iunmptlemfi  45427  sge0iunmptlemre  45429  sge0iunmpt  45432  sge0ltfirpmpt2  45440  sge0isummpt2  45446  sge0xaddlem2  45448  sge0xadd  45449  meadjiun  45480  voliunsge0lem  45486  meaiunincf  45497  meaiuninc3  45499  meaiininc  45501  hoimbl2  45679  vonhoire  45686  vonn0ioo2  45704  vonn0icc2  45706  salpreimagtlt  45744