Theorem chvarfv 2279

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  csbhypf  3882  axrep2  5243  axrep3  5244  isso2i  5608  frpoinsg  6348  tfindes  7861  findes  7899  dfoprab4f  8055  dom2lem  8991  setinds  9721  frinsg  9726  pwfseqlem4a  10657  pwfseqlem4  10658  uzind4s  12944  seqof2  14110  fsumclf  15808  fsumsplitf  15812  fproddivf  16060  fprodsplitf  16061  gsumcom2  20069  mdetralt2  22796  mdetunilem2  22800  ptcldmpt  23802  elmptrab  24015  isfildlem  24045  dvmptfsum  26165  dvfsumlem2  26217  lgamgulmlem2  27225  fmptcof2  33049  aciunf1lem  33054  fsumiunle  33219  esum2dlem  34522  fiunelros  34605  measiun  34649  bnj849  35354  bnj1014  35390  bnj1384  35461  bnj1489  35485  bnj1497  35489  finxpreclem6  38075  ptrest  38303  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  fdc1  38430  fsumshftd  39759  fphpd  43576  monotuz  43701  monotoddzz  43703  oddcomabszz  43704  setindtrs  43785  flcidc  43930  binomcxplemnotnn0  45099  fiiuncl  45818  disjf1  45934  disjinfi  45943  supxrleubrnmptf  46198  monoordxr  46229  monoord2xr  46231  fsummulc1f  46320  fsumnncl  46321  fsumf1of  46323  fsumiunss  46324  fsumreclf  46325  fsumlessf  46326  fsumsermpt  46328  fmul01  46329  fmuldfeq  46332  fmul01lt1lem1  46333  fmul01lt1lem2  46334  fprodexp  46343  fprodabs2  46344  climmulf  46353  climexp  46354  climsuse  46357  climrecf  46358  climinff  46360  climaddf  46364  mullimc  46365  neglimc  46394  addlimc  46395  0ellimcdiv  46396  climsubmpt  46407  climreclf  46411  climeldmeqmpt  46415  climfveqmpt  46418  fnlimfvre  46421  climfveqf  46427  climfveqmpt3  46429  climeldmeqf  46430  climeqf  46435  climeldmeqmpt3  46436  climinf2  46454  climinf2mpt  46461  climinfmpt  46462  limsupequz  46470  limsupequzmptf  46478  fprodcncf  46647  dvmptmulf  46684  dvnmptdivc  46685  dvnmul  46690  dvmptfprod  46692  stoweidlem3  46750  stoweidlem34  46781  stoweidlem42  46789  stoweidlem48  46795  fourierdlem112  46965  sge0lempt  47157  sge0iunmptlemfi  47160  sge0iunmptlemre  47162  sge0iunmpt  47165  sge0ltfirpmpt2  47173  sge0isummpt2  47179  sge0xaddlem2  47181  sge0xadd  47182  meadjiun  47213  voliunsge0lem  47219  meaiunincf  47230  meaiuninc3  47232  meaiininc  47234  hoimbl2  47412  vonhoire  47419  vonn0ioo2  47437  vonn0icc2  47439  salpreimagtlt  47477