Theorem chvarfv 2233

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  csbhypf  3922  axrep2  5288  axrep3  5289  isso2i  5623  frpoinsg  6344  wfisgOLD  6355  tfindes  7851  findes  7892  dfoprab4f  8041  dom2lem  8987  frinsg  9745  pwfseqlem4a  10655  pwfseqlem4  10656  uzind4s  12891  seqof2  14025  fsumclf  15683  fsumsplitf  15687  fproddivf  15930  fprodsplitf  15931  gsumcom2  19842  mdetralt2  22110  mdetunilem2  22114  ptcldmpt  23117  elmptrab  23330  isfildlem  23360  dvmptfsum  25491  dvfsumlem2  25543  lgamgulmlem2  26531  fmptcof2  31877  aciunf1lem  31882  fsumiunle  32030  esum2dlem  33085  fiunelros  33167  measiun  33211  bnj849  33931  bnj1014  33967  bnj1384  34038  bnj1489  34062  bnj1497  34066  setinds  34745  gg-dvfsumlem2  35178  finxpreclem6  36272  ptrest  36482  poimirlem24  36507  poimirlem25  36508  poimirlem26  36509  fdc1  36609  fsumshftd  37817  fphpd  41544  monotuz  41670  monotoddzz  41672  oddcomabszz  41673  setindtrs  41754  flcidc  41906  binomcxplemnotnn0  43105  fiiuncl  43742  disjf1  43870  disjinfi  43881  supxrleubrnmptf  44151  monoordxr  44183  monoord2xr  44185  fsummulc1f  44277  fsumnncl  44278  fsumf1of  44280  fsumiunss  44281  fsumreclf  44282  fsumlessf  44283  fsumsermpt  44285  fmul01  44286  fmuldfeq  44289  fmul01lt1lem1  44290  fmul01lt1lem2  44291  fprodexp  44300  fprodabs2  44301  climmulf  44310  climexp  44311  climsuse  44314  climrecf  44315  climinff  44317  climaddf  44321  mullimc  44322  neglimc  44353  addlimc  44354  0ellimcdiv  44355  climsubmpt  44366  climreclf  44370  climeldmeqmpt  44374  climfveqmpt  44377  fnlimfvre  44380  climfveqf  44386  climfveqmpt3  44388  climeldmeqf  44389  climeqf  44394  climeldmeqmpt3  44395  climinf2  44413  climinf2mpt  44420  climinfmpt  44421  limsupequz  44429  limsupequzmptf  44437  fprodcncf  44606  dvmptmulf  44643  dvnmptdivc  44644  dvnmul  44649  dvmptfprod  44651  stoweidlem3  44709  stoweidlem34  44740  stoweidlem42  44748  stoweidlem48  44754  fourierdlem112  44924  sge0lempt  45116  sge0iunmptlemfi  45119  sge0iunmptlemre  45121  sge0iunmpt  45124  sge0ltfirpmpt2  45132  sge0isummpt2  45138  sge0xaddlem2  45140  sge0xadd  45141  meadjiun  45172  voliunsge0lem  45178  meaiunincf  45189  meaiuninc3  45191  meaiininc  45193  hoimbl2  45371  vonhoire  45378  vonn0ioo2  45396  vonn0icc2  45398  salpreimagtlt  45436