Theorem chvarfv 2241

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2400 with a disjoint variable condition, which does not require ax-13 2377. (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  3907  axrep2  5257  axrep3  5258  isso2i  5603  frpoinsg  6337  wfisgOLD  6348  tfindes  7863  findes  7901  dfoprab4f  8060  dom2lem  9011  frinsg  9770  pwfseqlem4a  10680  pwfseqlem4  10681  uzind4s  12929  seqof2  14083  fsumclf  15759  fsumsplitf  15763  fproddivf  16008  fprodsplitf  16009  gsumcom2  19961  mdetralt2  22552  mdetunilem2  22556  ptcldmpt  23557  elmptrab  23770  isfildlem  23800  dvmptfsum  25936  dvfsumlem2  25990  dvfsumlem2OLD  25991  lgamgulmlem2  26997  fmptcof2  32640  aciunf1lem  32645  fsumiunle  32813  esum2dlem  34128  fiunelros  34210  measiun  34254  bnj849  34961  bnj1014  34997  bnj1384  35068  bnj1489  35092  bnj1497  35096  setinds  35801  finxpreclem6  37419  ptrest  37648  poimirlem24  37673  poimirlem25  37674  poimirlem26  37675  fdc1  37775  fsumshftd  38975  fphpd  42806  monotuz  42932  monotoddzz  42934  oddcomabszz  42935  setindtrs  43016  flcidc  43161  binomcxplemnotnn0  44347  fiiuncl  45056  disjf1  45174  disjinfi  45183  supxrleubrnmptf  45445  monoordxr  45476  monoord2xr  45478  fsummulc1f  45567  fsumnncl  45568  fsumf1of  45570  fsumiunss  45571  fsumreclf  45572  fsumlessf  45573  fsumsermpt  45575  fmul01  45576  fmuldfeq  45579  fmul01lt1lem1  45580  fmul01lt1lem2  45581  fprodexp  45590  fprodabs2  45591  climmulf  45600  climexp  45601  climsuse  45604  climrecf  45605  climinff  45607  climaddf  45611  mullimc  45612  neglimc  45643  addlimc  45644  0ellimcdiv  45645  climsubmpt  45656  climreclf  45660  climeldmeqmpt  45664  climfveqmpt  45667  fnlimfvre  45670  climfveqf  45676  climfveqmpt3  45678  climeldmeqf  45679  climeqf  45684  climeldmeqmpt3  45685  climinf2  45703  climinf2mpt  45710  climinfmpt  45711  limsupequz  45719  limsupequzmptf  45727  fprodcncf  45896  dvmptmulf  45933  dvnmptdivc  45934  dvnmul  45939  dvmptfprod  45941  stoweidlem3  45999  stoweidlem34  46030  stoweidlem42  46038  stoweidlem48  46044  fourierdlem112  46214  sge0lempt  46406  sge0iunmptlemfi  46409  sge0iunmptlemre  46411  sge0iunmpt  46414  sge0ltfirpmpt2  46422  sge0isummpt2  46428  sge0xaddlem2  46430  sge0xadd  46431  meadjiun  46462  voliunsge0lem  46468  meaiunincf  46479  meaiuninc3  46481  meaiininc  46483  hoimbl2  46661  vonhoire  46668  vonn0ioo2  46686  vonn0icc2  46688  salpreimagtlt  46726