Theorem chvarfv 2241

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2403 with a disjoint variable condition, which does not require ax-13 2380. (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 1795	1 ⊢ 𝜓

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782

This theorem is referenced by:  csbhypf  3950  axrep2  5306  axrep3  5307  isso2i  5644  frpoinsg  6375  wfisgOLD  6386  tfindes  7900  findes  7940  dfoprab4f  8097  dom2lem  9052  frinsg  9820  pwfseqlem4a  10730  pwfseqlem4  10731  uzind4s  12973  seqof2  14111  fsumclf  15786  fsumsplitf  15790  fproddivf  16035  fprodsplitf  16036  gsumcom2  20017  mdetralt2  22636  mdetunilem2  22640  ptcldmpt  23643  elmptrab  23856  isfildlem  23886  dvmptfsum  26033  dvfsumlem2  26087  dvfsumlem2OLD  26088  lgamgulmlem2  27091  fmptcof2  32675  aciunf1lem  32680  fsumiunle  32833  esum2dlem  34056  fiunelros  34138  measiun  34182  bnj849  34901  bnj1014  34937  bnj1384  35008  bnj1489  35032  bnj1497  35036  setinds  35742  finxpreclem6  37362  ptrest  37579  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  fdc1  37706  fsumshftd  38908  fphpd  42772  monotuz  42898  monotoddzz  42900  oddcomabszz  42901  setindtrs  42982  flcidc  43131  binomcxplemnotnn0  44325  fiiuncl  44967  disjf1  45090  disjinfi  45099  supxrleubrnmptf  45366  monoordxr  45398  monoord2xr  45400  fsummulc1f  45492  fsumnncl  45493  fsumf1of  45495  fsumiunss  45496  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  fmul01  45501  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  fprodexp  45515  fprodabs2  45516  climmulf  45525  climexp  45526  climsuse  45529  climrecf  45530  climinff  45532  climaddf  45536  mullimc  45537  neglimc  45568  addlimc  45569  0ellimcdiv  45570  climsubmpt  45581  climreclf  45585  climeldmeqmpt  45589  climfveqmpt  45592  fnlimfvre  45595  climfveqf  45601  climfveqmpt3  45603  climeldmeqf  45604  climeqf  45609  climeldmeqmpt3  45610  climinf2  45628  climinf2mpt  45635  climinfmpt  45636  limsupequz  45644  limsupequzmptf  45652  fprodcncf  45821  dvmptmulf  45858  dvnmptdivc  45859  dvnmul  45864  dvmptfprod  45866  stoweidlem3  45924  stoweidlem34  45955  stoweidlem42  45963  stoweidlem48  45969  fourierdlem112  46139  sge0lempt  46331  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  meadjiun  46387  voliunsge0lem  46393  meaiunincf  46404  meaiuninc3  46406  meaiininc  46408  hoimbl2  46586  vonhoire  46593  vonn0ioo2  46611  vonn0icc2  46613  salpreimagtlt  46651