Theorem chvarfv 2247

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2399 with a disjoint variable condition, which does not require ax-13 2376. (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 2246	. 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 2184

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

This theorem is referenced by:  csbhypf  3877  axrep2  5227  axrep3  5228  isso2i  5569  frpoinsg  6301  tfindes  7805  findes  7842  dfoprab4f  8000  dom2lem  8929  setinds  9658  frinsg  9663  pwfseqlem4a  10572  pwfseqlem4  10573  uzind4s  12821  seqof2  13983  fsumclf  15661  fsumsplitf  15665  fproddivf  15910  fprodsplitf  15911  gsumcom2  19904  mdetralt2  22553  mdetunilem2  22557  ptcldmpt  23558  elmptrab  23771  isfildlem  23801  dvmptfsum  25935  dvfsumlem2  25989  dvfsumlem2OLD  25990  lgamgulmlem2  26996  fmptcof2  32735  aciunf1lem  32740  fsumiunle  32910  esum2dlem  34249  fiunelros  34331  measiun  34375  bnj849  35081  bnj1014  35117  bnj1384  35188  bnj1489  35212  bnj1497  35216  finxpreclem6  37601  ptrest  37820  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  fdc1  37947  fsumshftd  39212  fphpd  43058  monotuz  43183  monotoddzz  43185  oddcomabszz  43186  setindtrs  43267  flcidc  43412  binomcxplemnotnn0  44597  fiiuncl  45310  disjf1  45427  disjinfi  45436  supxrleubrnmptf  45695  monoordxr  45726  monoord2xr  45728  fsummulc1f  45817  fsumnncl  45818  fsumf1of  45820  fsumiunss  45821  fsumreclf  45822  fsumlessf  45823  fsumsermpt  45825  fmul01  45826  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  fprodexp  45840  fprodabs2  45841  climmulf  45850  climexp  45851  climsuse  45854  climrecf  45855  climinff  45857  climaddf  45861  mullimc  45862  neglimc  45891  addlimc  45892  0ellimcdiv  45893  climsubmpt  45904  climreclf  45908  climeldmeqmpt  45912  climfveqmpt  45915  fnlimfvre  45918  climfveqf  45924  climfveqmpt3  45926  climeldmeqf  45927  climeqf  45932  climeldmeqmpt3  45933  climinf2  45951  climinf2mpt  45958  climinfmpt  45959  limsupequz  45967  limsupequzmptf  45975  fprodcncf  46144  dvmptmulf  46181  dvnmptdivc  46182  dvnmul  46187  dvmptfprod  46189  stoweidlem3  46247  stoweidlem34  46278  stoweidlem42  46286  stoweidlem48  46292  fourierdlem112  46462  sge0lempt  46654  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  sge0ltfirpmpt2  46670  sge0isummpt2  46676  sge0xaddlem2  46678  sge0xadd  46679  meadjiun  46710  voliunsge0lem  46716  meaiunincf  46727  meaiuninc3  46729  meaiininc  46731  hoimbl2  46909  vonhoire  46916  vonn0ioo2  46934  vonn0icc2  46936  salpreimagtlt  46974