Theorem chvarfv 2274

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803

This theorem is referenced by:  csbhypf  3878  axrep2  5227  axrep3  5228  isso2i  5588  frpoinsg  6325  tfindes  7838  findes  7876  dfoprab4f  8032  dom2lem  8967  setinds  9698  frinsg  9703  pwfseqlem4a  10613  pwfseqlem4  10614  uzind4s  12903  seqof2  14067  fsumclf  15756  fsumsplitf  15760  fproddivf  16008  fprodsplitf  16009  gsumcom2  20006  mdetralt2  22657  mdetunilem2  22661  ptcldmpt  23662  elmptrab  23875  isfildlem  23905  dvmptfsum  26025  dvfsumlem2  26077  lgamgulmlem2  27082  fmptcof2  32820  aciunf1lem  32825  fsumiunle  32992  esum2dlem  34350  fiunelros  34432  measiun  34476  bnj849  35181  bnj1014  35217  bnj1384  35288  bnj1489  35312  bnj1497  35316  finxpreclem6  37851  ptrest  38079  poimirlem24  38104  poimirlem25  38105  poimirlem26  38106  fdc1  38206  fsumshftd  39537  fphpd  43354  monotuz  43479  monotoddzz  43481  oddcomabszz  43482  setindtrs  43563  flcidc  43708  binomcxplemnotnn0  44893  fiiuncl  45606  disjf1  45722  disjinfi  45731  supxrleubrnmptf  45986  monoordxr  46017  monoord2xr  46019  fsummulc1f  46108  fsumnncl  46109  fsumf1of  46111  fsumiunss  46112  fsumreclf  46113  fsumlessf  46114  fsumsermpt  46116  fmul01  46117  fmuldfeq  46120  fmul01lt1lem1  46121  fmul01lt1lem2  46122  fprodexp  46131  fprodabs2  46132  climmulf  46141  climexp  46142  climsuse  46145  climrecf  46146  climinff  46148  climaddf  46152  mullimc  46153  neglimc  46182  addlimc  46183  0ellimcdiv  46184  climsubmpt  46195  climreclf  46199  climeldmeqmpt  46203  climfveqmpt  46206  fnlimfvre  46209  climfveqf  46215  climfveqmpt3  46217  climeldmeqf  46218  climeqf  46223  climeldmeqmpt3  46224  climinf2  46242  climinf2mpt  46249  climinfmpt  46250  limsupequz  46258  limsupequzmptf  46266  fprodcncf  46435  dvmptmulf  46472  dvnmptdivc  46473  dvnmul  46478  dvmptfprod  46480  stoweidlem3  46538  stoweidlem34  46569  stoweidlem42  46577  stoweidlem48  46583  fourierdlem112  46753  sge0lempt  46945  sge0iunmptlemfi  46948  sge0iunmptlemre  46950  sge0iunmpt  46953  sge0ltfirpmpt2  46961  sge0isummpt2  46967  sge0xaddlem2  46969  sge0xadd  46970  meadjiun  47001  voliunsge0lem  47007  meaiunincf  47018  meaiuninc3  47020  meaiininc  47022  hoimbl2  47200  vonhoire  47207  vonn0ioo2  47225  vonn0icc2  47227  salpreimagtlt  47265