Theorem chvarfv 2276

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  csbhypf  3875  axrep2  5235  axrep3  5236  isso2i  5600  frpoinsg  6341  tfindes  7859  findes  7897  dfoprab4f  8053  dom2lem  8998  setinds  9728  frinsg  9733  pwfseqlem4a  10670  pwfseqlem4  10671  uzind4s  12957  seqof2  14124  fsumclf  15824  fsumsplitf  15828  fproddivf  16074  fprodsplitf  16075  gsumcom2  20102  mdetralt2  22831  mdetunilem2  22835  ptcldmpt  23840  elmptrab  24053  isfildlem  24083  dvmptfsum  26202  dvfsumlem2  26254  lgamgulmlem2  27266  fmptcof2  33130  aciunf1lem  33135  fsumiunle  33299  esum2dlem  34602  fiunelros  34685  measiun  34729  bnj849  35434  bnj1014  35470  bnj1384  35541  bnj1489  35565  bnj1497  35569  finxpreclem6  38150  ptrest  38368  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  fdc1  38496  fsumshftd  39825  fphpd  43657  monotuz  43782  monotoddzz  43784  oddcomabszz  43785  setindtrs  43866  flcidc  44011  binomcxplemnotnn0  45180  fiiuncl  45899  disjf1  46015  disjinfi  46024  supxrleubrnmptf  46279  monoordxr  46310  monoord2xr  46312  fsummulc1f  46401  fsumnncl  46402  fsumf1of  46404  fsumiunss  46405  fsumreclf  46406  fsumlessf  46407  fsumsermpt  46409  fmul01  46410  fmuldfeq  46413  fmul01lt1lem1  46414  fmul01lt1lem2  46415  fprodexp  46424  fprodabs2  46425  climmulf  46434  climexp  46435  climsuse  46438  climrecf  46439  climinff  46441  climaddf  46445  mullimc  46446  neglimc  46475  addlimc  46476  0ellimcdiv  46477  climsubmpt  46488  climreclf  46492  climeldmeqmpt  46496  climfveqmpt  46499  fnlimfvre  46502  climfveqf  46508  climfveqmpt3  46510  climeldmeqf  46511  climeqf  46516  climeldmeqmpt3  46517  climinf2  46535  climinf2mpt  46542  climinfmpt  46543  limsupequz  46551  limsupequzmptf  46559  fprodcncf  46728  dvmptmulf  46765  dvnmptdivc  46766  dvnmul  46771  dvmptfprod  46773  stoweidlem3  46831  stoweidlem34  46862  stoweidlem42  46870  stoweidlem48  46876  fourierdlem112  47046  sge0lempt  47238  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  sge0ltfirpmpt2  47254  sge0isummpt2  47260  sge0xaddlem2  47262  sge0xadd  47263  meadjiun  47294  voliunsge0lem  47300  meaiunincf  47311  meaiuninc3  47313  meaiininc  47315  hoimbl2  47493  vonhoire  47500  vonn0ioo2  47518  vonn0icc2  47520  salpreimagtlt  47558