Theorem chvarfv 2248

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  csbhypf  3879  axrep2  5229  axrep3  5230  isso2i  5577  frpoinsg  6309  tfindes  7815  findes  7852  dfoprab4f  8010  dom2lem  8941  setinds  9670  frinsg  9675  pwfseqlem4a  10584  pwfseqlem4  10585  uzind4s  12833  seqof2  13995  fsumclf  15673  fsumsplitf  15677  fproddivf  15922  fprodsplitf  15923  gsumcom2  19916  mdetralt2  22565  mdetunilem2  22569  ptcldmpt  23570  elmptrab  23783  isfildlem  23813  dvmptfsum  25947  dvfsumlem2  26001  dvfsumlem2OLD  26002  lgamgulmlem2  27008  fmptcof2  32747  aciunf1lem  32752  fsumiunle  32921  esum2dlem  34270  fiunelros  34352  measiun  34396  bnj849  35101  bnj1014  35137  bnj1384  35208  bnj1489  35232  bnj1497  35236  finxpreclem6  37651  ptrest  37870  poimirlem24  37895  poimirlem25  37896  poimirlem26  37897  fdc1  37997  fsumshftd  39328  fphpd  43173  monotuz  43298  monotoddzz  43300  oddcomabszz  43301  setindtrs  43382  flcidc  43527  binomcxplemnotnn0  44712  fiiuncl  45425  disjf1  45542  disjinfi  45551  supxrleubrnmptf  45809  monoordxr  45840  monoord2xr  45842  fsummulc1f  45931  fsumnncl  45932  fsumf1of  45934  fsumiunss  45935  fsumreclf  45936  fsumlessf  45937  fsumsermpt  45939  fmul01  45940  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  fprodexp  45954  fprodabs2  45955  climmulf  45964  climexp  45965  climsuse  45968  climrecf  45969  climinff  45971  climaddf  45975  mullimc  45976  neglimc  46005  addlimc  46006  0ellimcdiv  46007  climsubmpt  46018  climreclf  46022  climeldmeqmpt  46026  climfveqmpt  46029  fnlimfvre  46032  climfveqf  46038  climfveqmpt3  46040  climeldmeqf  46041  climeqf  46046  climeldmeqmpt3  46047  climinf2  46065  climinf2mpt  46072  climinfmpt  46073  limsupequz  46081  limsupequzmptf  46089  fprodcncf  46258  dvmptmulf  46295  dvnmptdivc  46296  dvnmul  46301  dvmptfprod  46303  stoweidlem3  46361  stoweidlem34  46392  stoweidlem42  46400  stoweidlem48  46406  fourierdlem112  46576  sge0lempt  46768  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0iunmpt  46776  sge0ltfirpmpt2  46784  sge0isummpt2  46790  sge0xaddlem2  46792  sge0xadd  46793  meadjiun  46824  voliunsge0lem  46830  meaiunincf  46841  meaiuninc3  46843  meaiininc  46845  hoimbl2  47023  vonhoire  47030  vonn0ioo2  47048  vonn0icc2  47050  salpreimagtlt  47088