Theorem chvarfv 2234

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2396 with a disjoint variable condition, which does not require ax-13 2373. (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 228	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spimfv 2233	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1800	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  csbhypf  3862  axrep2  5213  axrep3  5214  isso2i  5539  frpoinsg  6250  wfisgOLD  6261  tfindes  7718  findes  7758  dfoprab4f  7905  dom2lem  8789  frinsg  9518  pwfseqlem4a  10426  pwfseqlem4  10427  uzind4s  12657  seqof2  13790  fsumclf  15459  fsumsplitf  15463  fproddivf  15706  fprodsplitf  15707  gsumcom2  19585  mdetralt2  21767  mdetunilem2  21771  ptcldmpt  22774  elmptrab  22987  isfildlem  23017  dvmptfsum  25148  dvfsumlem2  25200  lgamgulmlem2  26188  fmptcof2  31003  aciunf1lem  31008  fsumiunle  31152  esum2dlem  32069  fiunelros  32151  measiun  32195  bnj849  32914  bnj1014  32950  bnj1384  33021  bnj1489  33045  bnj1497  33049  setinds  33763  finxpreclem6  35576  ptrest  35785  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  fdc1  35913  fsumshftd  36973  fphpd  40645  monotuz  40770  monotoddzz  40772  oddcomabszz  40773  setindtrs  40854  flcidc  41006  binomcxplemnotnn0  41981  fiiuncl  42620  disjf1  42727  disjinfi  42738  supxrleubrnmptf  42998  monoordxr  43030  monoord2xr  43032  fsummulc1f  43119  fsumnncl  43120  fsumf1of  43122  fsumiunss  43123  fsumreclf  43124  fsumlessf  43125  fsumsermpt  43127  fmul01  43128  fmuldfeq  43131  fmul01lt1lem1  43132  fmul01lt1lem2  43133  fprodexp  43142  fprodabs2  43143  climmulf  43152  climexp  43153  climsuse  43156  climrecf  43157  climinff  43159  climaddf  43163  mullimc  43164  neglimc  43195  addlimc  43196  0ellimcdiv  43197  climsubmpt  43208  climreclf  43212  climeldmeqmpt  43216  climfveqmpt  43219  fnlimfvre  43222  climfveqf  43228  climfveqmpt3  43230  climeldmeqf  43231  climeqf  43236  climeldmeqmpt3  43237  climinf2  43255  climinf2mpt  43262  climinfmpt  43263  limsupequz  43271  limsupequzmptf  43279  fprodcncf  43448  dvmptmulf  43485  dvnmptdivc  43486  dvnmul  43491  dvmptfprod  43493  stoweidlem3  43551  stoweidlem34  43582  stoweidlem42  43590  stoweidlem48  43596  fourierdlem112  43766  sge0lempt  43955  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0ltfirpmpt2  43971  sge0isummpt2  43977  sge0xaddlem2  43979  sge0xadd  43980  meadjiun  44011  voliunsge0lem  44017  meaiunincf  44028  meaiuninc3  44030  meaiininc  44032  hoimbl2  44210  vonhoire  44217  vonn0ioo2  44235  vonn0icc2  44237  salpreimagtlt  44275