Theorem chvarfv 2252

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 230	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2251	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1804	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791

This theorem is referenced by:  csbhypf  3859  axrep2  5202  axrep3  5203  isso2i  5563  frpoinsg  6294  tfindes  7803  findes  7840  dfoprab4f  7998  dom2lem  8929  setinds  9661  frinsg  9666  pwfseqlem4a  10575  pwfseqlem4  10576  uzind4s  12849  seqof2  14013  fsumclf  15691  fsumsplitf  15695  fproddivf  15943  fprodsplitf  15944  gsumcom2  19941  mdetralt2  22592  mdetunilem2  22596  ptcldmpt  23597  elmptrab  23810  isfildlem  23840  dvmptfsum  25960  dvfsumlem2  26012  lgamgulmlem2  27011  fmptcof2  32749  aciunf1lem  32754  fsumiunle  32921  esum2dlem  34276  fiunelros  34358  measiun  34402  bnj849  35107  bnj1014  35143  bnj1384  35214  bnj1489  35238  bnj1497  35242  finxpreclem6  37758  ptrest  37986  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  fdc1  38113  fsumshftd  39444  fphpd  43261  monotuz  43386  monotoddzz  43388  oddcomabszz  43389  setindtrs  43470  flcidc  43615  binomcxplemnotnn0  44800  fiiuncl  45513  disjf1  45630  disjinfi  45639  supxrleubrnmptf  45894  monoordxr  45925  monoord2xr  45927  fsummulc1f  46016  fsumnncl  46017  fsumf1of  46019  fsumiunss  46020  fsumreclf  46021  fsumlessf  46022  fsumsermpt  46024  fmul01  46025  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  fprodexp  46039  fprodabs2  46040  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  neglimc  46090  addlimc  46091  0ellimcdiv  46092  climsubmpt  46103  climreclf  46107  climeldmeqmpt  46111  climfveqmpt  46114  fnlimfvre  46117  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  climeqf  46131  climeldmeqmpt3  46132  climinf2  46150  climinf2mpt  46157  climinfmpt  46158  limsupequz  46166  limsupequzmptf  46174  fprodcncf  46343  dvmptmulf  46380  dvnmptdivc  46381  dvnmul  46386  dvmptfprod  46388  stoweidlem3  46446  stoweidlem34  46477  stoweidlem42  46485  stoweidlem48  46491  fourierdlem112  46661  sge0lempt  46853  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isummpt2  46875  sge0xaddlem2  46877  sge0xadd  46878  meadjiun  46909  voliunsge0lem  46915  meaiunincf  46926  meaiuninc3  46928  meaiininc  46930  hoimbl2  47108  vonhoire  47115  vonn0ioo2  47133  vonn0icc2  47135  salpreimagtlt  47173