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  3881  axrep2  5224  axrep3  5225  isso2i  5568  frpoinsg  6295  tfindes  7803  findes  7840  dfoprab4f  7998  dom2lem  8924  frinsg  9666  pwfseqlem4a  10574  pwfseqlem4  10575  uzind4s  12828  seqof2  13986  fsumclf  15664  fsumsplitf  15668  fproddivf  15913  fprodsplitf  15914  gsumcom2  19873  mdetralt2  22513  mdetunilem2  22517  ptcldmpt  23518  elmptrab  23731  isfildlem  23761  dvmptfsum  25896  dvfsumlem2  25950  dvfsumlem2OLD  25951  lgamgulmlem2  26957  fmptcof2  32619  aciunf1lem  32624  fsumiunle  32793  esum2dlem  34078  fiunelros  34160  measiun  34204  bnj849  34911  bnj1014  34947  bnj1384  35018  bnj1489  35042  bnj1497  35046  setinds  35771  finxpreclem6  37389  ptrest  37618  poimirlem24  37643  poimirlem25  37644  poimirlem26  37645  fdc1  37745  fsumshftd  38950  fphpd  42809  monotuz  42934  monotoddzz  42936  oddcomabszz  42937  setindtrs  43018  flcidc  43163  binomcxplemnotnn0  44349  fiiuncl  45063  disjf1  45181  disjinfi  45190  supxrleubrnmptf  45450  monoordxr  45481  monoord2xr  45483  fsummulc1f  45572  fsumnncl  45573  fsumf1of  45575  fsumiunss  45576  fsumreclf  45577  fsumlessf  45578  fsumsermpt  45580  fmul01  45581  fmuldfeq  45584  fmul01lt1lem1  45585  fmul01lt1lem2  45586  fprodexp  45595  fprodabs2  45596  climmulf  45605  climexp  45606  climsuse  45609  climrecf  45610  climinff  45612  climaddf  45616  mullimc  45617  neglimc  45648  addlimc  45649  0ellimcdiv  45650  climsubmpt  45661  climreclf  45665  climeldmeqmpt  45669  climfveqmpt  45672  fnlimfvre  45675  climfveqf  45681  climfveqmpt3  45683  climeldmeqf  45684  climeqf  45689  climeldmeqmpt3  45690  climinf2  45708  climinf2mpt  45715  climinfmpt  45716  limsupequz  45724  limsupequzmptf  45732  fprodcncf  45901  dvmptmulf  45938  dvnmptdivc  45939  dvnmul  45944  dvmptfprod  45946  stoweidlem3  46004  stoweidlem34  46035  stoweidlem42  46043  stoweidlem48  46049  fourierdlem112  46219  sge0lempt  46411  sge0iunmptlemfi  46414  sge0iunmptlemre  46416  sge0iunmpt  46419  sge0ltfirpmpt2  46427  sge0isummpt2  46433  sge0xaddlem2  46435  sge0xadd  46436  meadjiun  46467  voliunsge0lem  46473  meaiunincf  46484  meaiuninc3  46486  meaiininc  46488  hoimbl2  46666  vonhoire  46673  vonn0ioo2  46691  vonn0icc2  46693  salpreimagtlt  46731