Theorem chvarfv 2243

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2395 with a disjoint variable condition, which does not require ax-13 2372. (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 2242	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1798	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  csbhypf  3873  axrep2  5215  axrep3  5216  isso2i  5556  frpoinsg  6285  tfindes  7788  findes  7825  dfoprab4f  7983  dom2lem  8909  setinds  9634  frinsg  9639  pwfseqlem4a  10547  pwfseqlem4  10548  uzind4s  12801  seqof2  13962  fsumclf  15640  fsumsplitf  15644  fproddivf  15889  fprodsplitf  15890  gsumcom2  19882  mdetralt2  22519  mdetunilem2  22523  ptcldmpt  23524  elmptrab  23737  isfildlem  23767  dvmptfsum  25901  dvfsumlem2  25955  dvfsumlem2OLD  25956  lgamgulmlem2  26962  fmptcof2  32631  aciunf1lem  32636  fsumiunle  32804  esum2dlem  34097  fiunelros  34179  measiun  34223  bnj849  34929  bnj1014  34965  bnj1384  35036  bnj1489  35060  bnj1497  35064  finxpreclem6  37430  ptrest  37659  poimirlem24  37684  poimirlem25  37685  poimirlem26  37686  fdc1  37786  fsumshftd  38991  fphpd  42849  monotuz  42974  monotoddzz  42976  oddcomabszz  42977  setindtrs  43058  flcidc  43203  binomcxplemnotnn0  44389  fiiuncl  45102  disjf1  45220  disjinfi  45229  supxrleubrnmptf  45489  monoordxr  45520  monoord2xr  45522  fsummulc1f  45611  fsumnncl  45612  fsumf1of  45614  fsumiunss  45615  fsumreclf  45616  fsumlessf  45617  fsumsermpt  45619  fmul01  45620  fmuldfeq  45623  fmul01lt1lem1  45624  fmul01lt1lem2  45625  fprodexp  45634  fprodabs2  45635  climmulf  45644  climexp  45645  climsuse  45648  climrecf  45649  climinff  45651  climaddf  45655  mullimc  45656  neglimc  45685  addlimc  45686  0ellimcdiv  45687  climsubmpt  45698  climreclf  45702  climeldmeqmpt  45706  climfveqmpt  45709  fnlimfvre  45712  climfveqf  45718  climfveqmpt3  45720  climeldmeqf  45721  climeqf  45726  climeldmeqmpt3  45727  climinf2  45745  climinf2mpt  45752  climinfmpt  45753  limsupequz  45761  limsupequzmptf  45769  fprodcncf  45938  dvmptmulf  45975  dvnmptdivc  45976  dvnmul  45981  dvmptfprod  45983  stoweidlem3  46041  stoweidlem34  46072  stoweidlem42  46080  stoweidlem48  46086  fourierdlem112  46256  sge0lempt  46448  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  sge0iunmpt  46456  sge0ltfirpmpt2  46464  sge0isummpt2  46470  sge0xaddlem2  46472  sge0xadd  46473  meadjiun  46504  voliunsge0lem  46510  meaiunincf  46521  meaiuninc3  46523  meaiininc  46525  hoimbl2  46703  vonhoire  46710  vonn0ioo2  46728  vonn0icc2  46730  salpreimagtlt  46768