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 1829	1 ⊢ 𝜓

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  csbhypf  3874  axrep2  5234  axrep3  5235  isso2i  5595  frpoinsg  6346  tfindes  7875  findes  7913  dfoprab4f  8068  dom2lem  9023  setinds  9754  frinsg  9759  pwfseqlem4a  10750  pwfseqlem4  10751  uzind4s  13039  seqof2  14207  fsumclf  15910  fsumsplitf  15914  fproddivf  16160  fprodsplitf  16161  gsumcom2  20195  mdetralt2  22930  mdetunilem2  22934  ptcldmpt  23939  elmptrab  24152  isfildlem  24182  dvmptfsum  26301  dvfsumlem2  26353  lgamgulmlem2  27363  fmptcof2  33299  aciunf1lem  33304  fsumiunle  33467  esum2dlem  34771  fiunelros  34854  measiun  34898  bnj849  35602  bnj1014  35638  bnj1384  35709  bnj1489  35733  bnj1497  35737  finxpreclem6  38413  ptrest  38631  poimirlem24  38656  poimirlem25  38657  poimirlem26  38658  fdc1  38774  fsumshftd  40103  fphpd  43917  monotuz  44042  monotoddzz  44044  oddcomabszz  44045  setindtrs  44126  flcidc  44266  binomcxplemnotnn0  45434  fiiuncl  46176  disjf1  46292  disjinfi  46301  supxrleubrnmptf  46555  monoordxr  46586  monoord2xr  46588  fsummulc1f  46677  fsumnncl  46678  fsumf1of  46680  fsumiunss  46681  fsumreclf  46682  fsumlessf  46683  fsumsermpt  46685  fmul01  46686  fmuldfeq  46689  fmul01lt1lem1  46690  fmul01lt1lem2  46691  fprodexp  46700  fprodabs2  46701  climmulf  46710  climexp  46711  climsuse  46714  climrecf  46715  climinff  46717  climaddf  46721  mullimc  46722  neglimc  46751  addlimc  46752  0ellimcdiv  46753  climsubmpt  46764  climreclf  46768  climeldmeqmpt  46772  climfveqmpt  46775  fnlimfvre  46778  climfveqf  46784  climfveqmpt3  46786  climeldmeqf  46787  climeqf  46792  climeldmeqmpt3  46793  climinf2  46811  climinf2mpt  46818  climinfmpt  46819  limsupequz  46827  limsupequzmptf  46835  fprodcncf  47004  dvmptmulf  47041  dvnmptdivc  47042  dvnmul  47047  dvmptfprod  47049  stoweidlem3  47107  stoweidlem34  47138  stoweidlem42  47146  stoweidlem48  47152  fourierdlem112  47322  sge0lempt  47514  sge0iunmptlemfi  47517  sge0iunmptlemre  47519  sge0iunmpt  47522  sge0ltfirpmpt2  47530  sge0isummpt2  47536  sge0xaddlem2  47538  sge0xadd  47539  meadjiun  47570  voliunsge0lem  47576  meaiunincf  47587  meaiuninc3  47589  meaiininc  47591  hoimbl2  47769  vonhoire  47776  vonn0ioo2  47794  vonn0icc2  47796  salpreimagtlt  47834