Theorem chvarfv 2241

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2393 with a disjoint variable condition, which does not require ax-13 2370. (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 2240	. 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 2008  ax-12 2178

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

This theorem is referenced by:  csbhypf  3890  axrep2  5237  axrep3  5238  isso2i  5583  frpoinsg  6316  tfindes  7839  findes  7876  dfoprab4f  8035  dom2lem  8963  frinsg  9704  pwfseqlem4a  10614  pwfseqlem4  10615  uzind4s  12867  seqof2  14025  fsumclf  15704  fsumsplitf  15708  fproddivf  15953  fprodsplitf  15954  gsumcom2  19905  mdetralt2  22496  mdetunilem2  22500  ptcldmpt  23501  elmptrab  23714  isfildlem  23744  dvmptfsum  25879  dvfsumlem2  25933  dvfsumlem2OLD  25934  lgamgulmlem2  26940  fmptcof2  32581  aciunf1lem  32586  fsumiunle  32754  esum2dlem  34082  fiunelros  34164  measiun  34208  bnj849  34915  bnj1014  34951  bnj1384  35022  bnj1489  35046  bnj1497  35050  setinds  35766  finxpreclem6  37384  ptrest  37613  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  fdc1  37740  fsumshftd  38945  fphpd  42804  monotuz  42930  monotoddzz  42932  oddcomabszz  42933  setindtrs  43014  flcidc  43159  binomcxplemnotnn0  44345  fiiuncl  45059  disjf1  45177  disjinfi  45186  supxrleubrnmptf  45447  monoordxr  45478  monoord2xr  45480  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumiunss  45573  fsumreclf  45574  fsumlessf  45575  fsumsermpt  45577  fmul01  45578  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fprodexp  45592  fprodabs2  45593  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  neglimc  45645  addlimc  45646  0ellimcdiv  45647  climsubmpt  45658  climreclf  45662  climeldmeqmpt  45666  climfveqmpt  45669  fnlimfvre  45672  climfveqf  45678  climfveqmpt3  45680  climeldmeqf  45681  climeqf  45686  climeldmeqmpt3  45687  climinf2  45705  climinf2mpt  45712  climinfmpt  45713  limsupequz  45721  limsupequzmptf  45729  fprodcncf  45898  dvmptmulf  45935  dvnmptdivc  45936  dvnmul  45941  dvmptfprod  45943  stoweidlem3  46001  stoweidlem34  46032  stoweidlem42  46040  stoweidlem48  46046  fourierdlem112  46216  sge0lempt  46408  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  meadjiun  46464  voliunsge0lem  46470  meaiunincf  46481  meaiuninc3  46483  meaiininc  46485  hoimbl2  46663  vonhoire  46670  vonn0ioo2  46688  vonn0icc2  46690  salpreimagtlt  46728