Theorem chvarfv 2237

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2397 with a disjoint variable condition, which does not require ax-13 2374. (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 2236	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1793	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780

This theorem is referenced by:  csbhypf  3936  axrep2  5287  axrep3  5288  isso2i  5632  frpoinsg  6365  wfisgOLD  6376  tfindes  7883  findes  7922  dfoprab4f  8079  dom2lem  9030  frinsg  9788  pwfseqlem4a  10698  pwfseqlem4  10699  uzind4s  12947  seqof2  14097  fsumclf  15770  fsumsplitf  15774  fproddivf  16019  fprodsplitf  16020  gsumcom2  20007  mdetralt2  22630  mdetunilem2  22634  ptcldmpt  23637  elmptrab  23850  isfildlem  23880  dvmptfsum  26027  dvfsumlem2  26081  dvfsumlem2OLD  26082  lgamgulmlem2  27087  fmptcof2  32673  aciunf1lem  32678  fsumiunle  32835  esum2dlem  34072  fiunelros  34154  measiun  34198  bnj849  34917  bnj1014  34953  bnj1384  35024  bnj1489  35048  bnj1497  35052  setinds  35759  finxpreclem6  37378  ptrest  37605  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  fdc1  37732  fsumshftd  38933  fphpd  42803  monotuz  42929  monotoddzz  42931  oddcomabszz  42932  setindtrs  43013  flcidc  43158  binomcxplemnotnn0  44351  fiiuncl  45004  disjf1  45125  disjinfi  45134  supxrleubrnmptf  45400  monoordxr  45432  monoord2xr  45434  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumiunss  45530  fsumreclf  45531  fsumlessf  45532  fsumsermpt  45534  fmul01  45535  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fprodexp  45549  fprodabs2  45550  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climinff  45566  climaddf  45570  mullimc  45571  neglimc  45602  addlimc  45603  0ellimcdiv  45604  climsubmpt  45615  climreclf  45619  climeldmeqmpt  45623  climfveqmpt  45626  fnlimfvre  45629  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  climeqf  45643  climeldmeqmpt3  45644  climinf2  45662  climinf2mpt  45669  climinfmpt  45670  limsupequz  45678  limsupequzmptf  45686  fprodcncf  45855  dvmptmulf  45892  dvnmptdivc  45893  dvnmul  45898  dvmptfprod  45900  stoweidlem3  45958  stoweidlem34  45989  stoweidlem42  45997  stoweidlem48  46003  fourierdlem112  46173  sge0lempt  46365  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  meadjiun  46421  voliunsge0lem  46427  meaiunincf  46438  meaiuninc3  46440  meaiininc  46442  hoimbl2  46620  vonhoire  46627  vonn0ioo2  46645  vonn0icc2  46647  salpreimagtlt  46685