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  5242  axrep3  5243  isso2i  5604  frpoinsg  6342  tfindes  7855  findes  7893  dfoprab4f  8049  dom2lem  8985  setinds  9714  frinsg  9719  pwfseqlem4a  10642  pwfseqlem4  10643  uzind4s  12928  seqof2  14092  fsumclf  15785  fsumsplitf  15789  fproddivf  16037  fprodsplitf  16038  gsumcom2  20041  mdetralt2  22731  mdetunilem2  22735  ptcldmpt  23736  elmptrab  23949  isfildlem  23979  dvmptfsum  26099  dvfsumlem2  26151  lgamgulmlem2  27156  fmptcof2  32939  aciunf1lem  32944  fsumiunle  33110  esum2dlem  34423  fiunelros  34505  measiun  34549  bnj849  35254  bnj1014  35290  bnj1384  35361  bnj1489  35385  bnj1497  35389  finxpreclem6  37925  ptrest  38153  poimirlem24  38178  poimirlem25  38179  poimirlem26  38180  fdc1  38280  fsumshftd  39611  fphpd  43430  monotuz  43555  monotoddzz  43557  oddcomabszz  43558  setindtrs  43639  flcidc  43784  binomcxplemnotnn0  44953  fiiuncl  45672  disjf1  45788  disjinfi  45797  supxrleubrnmptf  46052  monoordxr  46083  monoord2xr  46085  fsummulc1f  46174  fsumnncl  46175  fsumf1of  46177  fsumiunss  46178  fsumreclf  46179  fsumlessf  46180  fsumsermpt  46182  fmul01  46183  fmuldfeq  46186  fmul01lt1lem1  46187  fmul01lt1lem2  46188  fprodexp  46197  fprodabs2  46198  climmulf  46207  climexp  46208  climsuse  46211  climrecf  46212  climinff  46214  climaddf  46218  mullimc  46219  neglimc  46248  addlimc  46249  0ellimcdiv  46250  climsubmpt  46261  climreclf  46265  climeldmeqmpt  46269  climfveqmpt  46272  fnlimfvre  46275  climfveqf  46281  climfveqmpt3  46283  climeldmeqf  46284  climeqf  46289  climeldmeqmpt3  46290  climinf2  46308  climinf2mpt  46315  climinfmpt  46316  limsupequz  46324  limsupequzmptf  46332  fprodcncf  46501  dvmptmulf  46538  dvnmptdivc  46539  dvnmul  46544  dvmptfprod  46546  stoweidlem3  46604  stoweidlem34  46635  stoweidlem42  46643  stoweidlem48  46649  fourierdlem112  46819  sge0lempt  47011  sge0iunmptlemfi  47014  sge0iunmptlemre  47016  sge0iunmpt  47019  sge0ltfirpmpt2  47027  sge0isummpt2  47033  sge0xaddlem2  47035  sge0xadd  47036  meadjiun  47067  voliunsge0lem  47073  meaiunincf  47084  meaiuninc3  47086  meaiininc  47088  hoimbl2  47266  vonhoire  47273  vonn0ioo2  47291  vonn0icc2  47293  salpreimagtlt  47331