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  3887  axrep2  5232  axrep3  5233  isso2i  5576  frpoinsg  6304  tfindes  7819  findes  7856  dfoprab4f  8014  dom2lem  8940  frinsg  9680  pwfseqlem4a  10590  pwfseqlem4  10591  uzind4s  12843  seqof2  14001  fsumclf  15680  fsumsplitf  15684  fproddivf  15929  fprodsplitf  15930  gsumcom2  19881  mdetralt2  22472  mdetunilem2  22476  ptcldmpt  23477  elmptrab  23690  isfildlem  23720  dvmptfsum  25855  dvfsumlem2  25909  dvfsumlem2OLD  25910  lgamgulmlem2  26916  fmptcof2  32554  aciunf1lem  32559  fsumiunle  32727  esum2dlem  34055  fiunelros  34137  measiun  34181  bnj849  34888  bnj1014  34924  bnj1384  34995  bnj1489  35019  bnj1497  35023  setinds  35739  finxpreclem6  37357  ptrest  37586  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  fdc1  37713  fsumshftd  38918  fphpd  42777  monotuz  42903  monotoddzz  42905  oddcomabszz  42906  setindtrs  42987  flcidc  43132  binomcxplemnotnn0  44318  fiiuncl  45032  disjf1  45150  disjinfi  45159  supxrleubrnmptf  45420  monoordxr  45451  monoord2xr  45453  fsummulc1f  45542  fsumnncl  45543  fsumf1of  45545  fsumiunss  45546  fsumreclf  45547  fsumlessf  45548  fsumsermpt  45550  fmul01  45551  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  fprodexp  45565  fprodabs2  45566  climmulf  45575  climexp  45576  climsuse  45579  climrecf  45580  climinff  45582  climaddf  45586  mullimc  45587  neglimc  45618  addlimc  45619  0ellimcdiv  45620  climsubmpt  45631  climreclf  45635  climeldmeqmpt  45639  climfveqmpt  45642  fnlimfvre  45645  climfveqf  45651  climfveqmpt3  45653  climeldmeqf  45654  climeqf  45659  climeldmeqmpt3  45660  climinf2  45678  climinf2mpt  45685  climinfmpt  45686  limsupequz  45694  limsupequzmptf  45702  fprodcncf  45871  dvmptmulf  45908  dvnmptdivc  45909  dvnmul  45914  dvmptfprod  45916  stoweidlem3  45974  stoweidlem34  46005  stoweidlem42  46013  stoweidlem48  46019  fourierdlem112  46189  sge0lempt  46381  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  sge0ltfirpmpt2  46397  sge0isummpt2  46403  sge0xaddlem2  46405  sge0xadd  46406  meadjiun  46437  voliunsge0lem  46443  meaiunincf  46454  meaiuninc3  46456  meaiininc  46458  hoimbl2  46636  vonhoire  46643  vonn0ioo2  46661  vonn0icc2  46663  salpreimagtlt  46701