Theorem chvarfv 2242

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2413 with a disjoint variable condition, which does not require ax-13 2390. (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 231	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2241	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1798	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 208  Ⅎ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 1970  ax-7 2015  ax-12 2177

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

This theorem is referenced by:  csbhypf  3911  axrep2  5193  axrep3  5194  opelopabsb  5417  isso2i  5508  wfisg  6183  tfindes  7577  findes  7612  dfoprab4f  7754  dom2lem  8549  pwfseqlem4a  10083  pwfseqlem4  10084  uzind4s  12309  seqof2  13429  fsumsplitf  15098  fproddivf  15341  fprodsplitf  15342  gsumcom2  19095  mdetralt2  21218  mdetunilem2  21222  ptcldmpt  22222  elmptrab  22435  isfildlem  22465  dvmptfsum  24572  dvfsumlem2  24624  lgamgulmlem2  25607  fmptcof2  30402  aciunf1lem  30407  fsumiunle  30545  esum2dlem  31351  fiunelros  31433  measiun  31477  bnj849  32197  bnj1014  32233  bnj1384  32304  bnj1489  32328  bnj1497  32332  setinds  33023  frpoinsg  33081  frinsg  33087  finxpreclem6  34680  ptrest  34906  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  fdc1  35036  fsumshftd  36103  fphpd  39462  monotuz  39587  monotoddzz  39589  oddcomabszz  39590  setindtrs  39671  flcidc  39823  binomcxplemnotnn0  40737  fiiuncl  41376  disjf1  41492  disjinfi  41503  supxrleubrnmptf  41776  monoordxr  41808  monoord2xr  41810  fsumclf  41899  fsummulc1f  41900  fsumnncl  41901  fsumf1of  41904  fsumiunss  41905  fsumreclf  41906  fsumlessf  41907  fsumsermpt  41909  fmul01  41910  fmuldfeq  41913  fmul01lt1lem1  41914  fmul01lt1lem2  41915  fprodexp  41924  fprodabs2  41925  climmulf  41934  climexp  41935  climsuse  41938  climrecf  41939  climinff  41941  climaddf  41945  mullimc  41946  neglimc  41977  addlimc  41978  0ellimcdiv  41979  climsubmpt  41990  climreclf  41994  climeldmeqmpt  41998  climfveqmpt  42001  fnlimfvre  42004  climfveqf  42010  climfveqmpt3  42012  climeldmeqf  42013  climeqf  42018  climeldmeqmpt3  42019  climinf2  42037  climinf2mpt  42044  climinfmpt  42045  limsupequz  42053  limsupequzmptf  42061  fprodcncf  42233  dvmptmulf  42271  dvnmptdivc  42272  dvnmul  42277  dvmptfprod  42279  stoweidlem3  42337  stoweidlem34  42368  stoweidlem42  42376  stoweidlem48  42382  fourierdlem112  42552  sge0lempt  42741  sge0iunmptlemfi  42744  sge0iunmptlemre  42746  sge0iunmpt  42749  sge0ltfirpmpt2  42757  sge0isummpt2  42763  sge0xaddlem2  42765  sge0xadd  42766  meadjiun  42797  voliunsge0lem  42803  meaiunincf  42814  meaiuninc3  42816  meaiininc  42818  hoimbl2  42996  vonhoire  43003  vonn0ioo2  43021  vonn0icc2  43023  salpreimagtlt  43056