Theorem chvarfv 2245

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 2244	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvarfv.2	. 2 ⊢ 𝜑
6	4, 5	mpg 1798	1 ⊢ 𝜓

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  csbhypf  3874  axrep2  5224  axrep3  5225  isso2i  5566  frpoinsg  6298  tfindes  7802  findes  7839  dfoprab4f  7997  dom2lem  8925  setinds  9650  frinsg  9655  pwfseqlem4a  10563  pwfseqlem4  10564  uzind4s  12812  seqof2  13974  fsumclf  15652  fsumsplitf  15656  fproddivf  15901  fprodsplitf  15902  gsumcom2  19895  mdetralt2  22544  mdetunilem2  22548  ptcldmpt  23549  elmptrab  23762  isfildlem  23792  dvmptfsum  25926  dvfsumlem2  25980  dvfsumlem2OLD  25981  lgamgulmlem2  26987  fmptcof2  32661  aciunf1lem  32666  fsumiunle  32838  esum2dlem  34177  fiunelros  34259  measiun  34303  bnj849  35009  bnj1014  35045  bnj1384  35116  bnj1489  35140  bnj1497  35144  finxpreclem6  37513  ptrest  37732  poimirlem24  37757  poimirlem25  37758  poimirlem26  37759  fdc1  37859  fsumshftd  39124  fphpd  42973  monotuz  43098  monotoddzz  43100  oddcomabszz  43101  setindtrs  43182  flcidc  43327  binomcxplemnotnn0  44513  fiiuncl  45226  disjf1  45343  disjinfi  45352  supxrleubrnmptf  45611  monoordxr  45642  monoord2xr  45644  fsummulc1f  45733  fsumnncl  45734  fsumf1of  45736  fsumiunss  45737  fsumreclf  45738  fsumlessf  45739  fsumsermpt  45741  fmul01  45742  fmuldfeq  45745  fmul01lt1lem1  45746  fmul01lt1lem2  45747  fprodexp  45756  fprodabs2  45757  climmulf  45766  climexp  45767  climsuse  45770  climrecf  45771  climinff  45773  climaddf  45777  mullimc  45778  neglimc  45807  addlimc  45808  0ellimcdiv  45809  climsubmpt  45820  climreclf  45824  climeldmeqmpt  45828  climfveqmpt  45831  fnlimfvre  45834  climfveqf  45840  climfveqmpt3  45842  climeldmeqf  45843  climeqf  45848  climeldmeqmpt3  45849  climinf2  45867  climinf2mpt  45874  climinfmpt  45875  limsupequz  45883  limsupequzmptf  45891  fprodcncf  46060  dvmptmulf  46097  dvnmptdivc  46098  dvnmul  46103  dvmptfprod  46105  stoweidlem3  46163  stoweidlem34  46194  stoweidlem42  46202  stoweidlem48  46208  fourierdlem112  46378  sge0lempt  46570  sge0iunmptlemfi  46573  sge0iunmptlemre  46575  sge0iunmpt  46578  sge0ltfirpmpt2  46586  sge0isummpt2  46592  sge0xaddlem2  46594  sge0xadd  46595  meadjiun  46626  voliunsge0lem  46632  meaiunincf  46643  meaiuninc3  46645  meaiininc  46647  hoimbl2  46825  vonhoire  46832  vonn0ioo2  46850  vonn0icc2  46852  salpreimagtlt  46890