Theorem chvarfv 2241

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  csbhypf  3875  axrep2  5217  axrep3  5218  isso2i  5558  frpoinsg  6285  tfindes  7787  findes  7824  dfoprab4f  7982  dom2lem  8908  frinsg  9635  pwfseqlem4a  10543  pwfseqlem4  10544  uzind4s  12797  seqof2  13955  fsumclf  15632  fsumsplitf  15636  fproddivf  15881  fprodsplitf  15882  gsumcom2  19841  mdetralt2  22478  mdetunilem2  22482  ptcldmpt  23483  elmptrab  23696  isfildlem  23726  dvmptfsum  25860  dvfsumlem2  25914  dvfsumlem2OLD  25915  lgamgulmlem2  26921  fmptcof2  32591  aciunf1lem  32596  fsumiunle  32767  esum2dlem  34073  fiunelros  34155  measiun  34199  bnj849  34905  bnj1014  34941  bnj1384  35012  bnj1489  35036  bnj1497  35040  setinds  35769  finxpreclem6  37387  ptrest  37616  poimirlem24  37641  poimirlem25  37642  poimirlem26  37643  fdc1  37743  fsumshftd  38948  fphpd  42806  monotuz  42931  monotoddzz  42933  oddcomabszz  42934  setindtrs  43015  flcidc  43160  binomcxplemnotnn0  44346  fiiuncl  45059  disjf1  45177  disjinfi  45186  supxrleubrnmptf  45446  monoordxr  45477  monoord2xr  45479  fsummulc1f  45568  fsumnncl  45569  fsumf1of  45571  fsumiunss  45572  fsumreclf  45573  fsumlessf  45574  fsumsermpt  45576  fmul01  45577  fmuldfeq  45580  fmul01lt1lem1  45581  fmul01lt1lem2  45582  fprodexp  45591  fprodabs2  45592  climmulf  45601  climexp  45602  climsuse  45605  climrecf  45606  climinff  45608  climaddf  45612  mullimc  45613  neglimc  45642  addlimc  45643  0ellimcdiv  45644  climsubmpt  45655  climreclf  45659  climeldmeqmpt  45663  climfveqmpt  45666  fnlimfvre  45669  climfveqf  45675  climfveqmpt3  45677  climeldmeqf  45678  climeqf  45683  climeldmeqmpt3  45684  climinf2  45702  climinf2mpt  45709  climinfmpt  45710  limsupequz  45718  limsupequzmptf  45726  fprodcncf  45895  dvmptmulf  45932  dvnmptdivc  45933  dvnmul  45938  dvmptfprod  45940  stoweidlem3  45998  stoweidlem34  46029  stoweidlem42  46037  stoweidlem48  46043  fourierdlem112  46213  sge0lempt  46405  sge0iunmptlemfi  46408  sge0iunmptlemre  46410  sge0iunmpt  46413  sge0ltfirpmpt2  46421  sge0isummpt2  46427  sge0xaddlem2  46429  sge0xadd  46430  meadjiun  46461  voliunsge0lem  46467  meaiunincf  46478  meaiuninc3  46480  meaiininc  46482  hoimbl2  46660  vonhoire  46667  vonn0ioo2  46685  vonn0icc2  46687  salpreimagtlt  46725