Theorem chvarfv 2282

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811

This theorem is referenced by:  csbhypf  3889  axrep2  5245  axrep3  5246  isso2i  5607  frpoinsg  6345  tfindes  7858  findes  7896  dfoprab4f  8052  dom2lem  8988  setinds  9717  frinsg  9722  pwfseqlem4a  10645  pwfseqlem4  10646  uzind4s  12931  seqof2  14095  fsumclf  15788  fsumsplitf  15792  fproddivf  16040  fprodsplitf  16041  gsumcom2  20044  mdetralt2  22734  mdetunilem2  22738  ptcldmpt  23739  elmptrab  23952  isfildlem  23982  dvmptfsum  26102  dvfsumlem2  26154  lgamgulmlem2  27159  fmptcof2  32942  aciunf1lem  32947  fsumiunle  33113  esum2dlem  34426  fiunelros  34508  measiun  34552  bnj849  35257  bnj1014  35293  bnj1384  35364  bnj1489  35388  bnj1497  35392  finxpreclem6  37929  ptrest  38157  poimirlem24  38182  poimirlem25  38183  poimirlem26  38184  fdc1  38284  fsumshftd  39615  fphpd  43434  monotuz  43559  monotoddzz  43561  oddcomabszz  43562  setindtrs  43643  flcidc  43788  binomcxplemnotnn0  44957  fiiuncl  45676  disjf1  45792  disjinfi  45801  supxrleubrnmptf  46056  monoordxr  46087  monoord2xr  46089  fsummulc1f  46178  fsumnncl  46179  fsumf1of  46181  fsumiunss  46182  fsumreclf  46183  fsumlessf  46184  fsumsermpt  46186  fmul01  46187  fmuldfeq  46190  fmul01lt1lem1  46191  fmul01lt1lem2  46192  fprodexp  46201  fprodabs2  46202  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climinff  46218  climaddf  46222  mullimc  46223  neglimc  46252  addlimc  46253  0ellimcdiv  46254  climsubmpt  46265  climreclf  46269  climeldmeqmpt  46273  climfveqmpt  46276  fnlimfvre  46279  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  climeqf  46293  climeldmeqmpt3  46294  climinf2  46312  climinf2mpt  46319  climinfmpt  46320  limsupequz  46328  limsupequzmptf  46336  fprodcncf  46505  dvmptmulf  46542  dvnmptdivc  46543  dvnmul  46548  dvmptfprod  46550  stoweidlem3  46608  stoweidlem34  46639  stoweidlem42  46647  stoweidlem48  46653  fourierdlem112  46823  sge0lempt  47015  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0iunmpt  47023  sge0ltfirpmpt2  47031  sge0isummpt2  47037  sge0xaddlem2  47039  sge0xadd  47040  meadjiun  47071  voliunsge0lem  47077  meaiunincf  47088  meaiuninc3  47090  meaiininc  47092  hoimbl2  47270  vonhoire  47277  vonn0ioo2  47295  vonn0icc2  47297  salpreimagtlt  47335