Theorem chvarfv 2276

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  csbhypf  3881  axrep2  5241  axrep3  5242  isso2i  5606  frpoinsg  6344  tfindes  7855  findes  7893  dfoprab4f  8049  dom2lem  8985  setinds  9714  frinsg  9719  pwfseqlem4a  10641  pwfseqlem4  10642  uzind4s  12927  seqof2  14092  fsumclf  15785  fsumsplitf  15789  fproddivf  16037  fprodsplitf  16038  gsumcom2  20040  mdetralt2  22766  mdetunilem2  22770  ptcldmpt  23771  elmptrab  23984  isfildlem  24014  dvmptfsum  26134  dvfsumlem2  26186  lgamgulmlem2  27194  fmptcof2  33002  aciunf1lem  33007  fsumiunle  33173  esum2dlem  34482  fiunelros  34564  measiun  34608  bnj849  35313  bnj1014  35349  bnj1384  35420  bnj1489  35444  bnj1497  35448  finxpreclem6  38042  ptrest  38270  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  fdc1  38397  fsumshftd  39726  fphpd  43543  monotuz  43668  monotoddzz  43670  oddcomabszz  43671  setindtrs  43752  flcidc  43897  binomcxplemnotnn0  45066  fiiuncl  45785  disjf1  45901  disjinfi  45910  supxrleubrnmptf  46165  monoordxr  46196  monoord2xr  46198  fsummulc1f  46287  fsumnncl  46288  fsumf1of  46290  fsumiunss  46291  fsumreclf  46292  fsumlessf  46293  fsumsermpt  46295  fmul01  46296  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  fprodexp  46310  fprodabs2  46311  climmulf  46320  climexp  46321  climsuse  46324  climrecf  46325  climinff  46327  climaddf  46331  mullimc  46332  neglimc  46361  addlimc  46362  0ellimcdiv  46363  climsubmpt  46374  climreclf  46378  climeldmeqmpt  46382  climfveqmpt  46385  fnlimfvre  46388  climfveqf  46394  climfveqmpt3  46396  climeldmeqf  46397  climeqf  46402  climeldmeqmpt3  46403  climinf2  46421  climinf2mpt  46428  climinfmpt  46429  limsupequz  46437  limsupequzmptf  46445  fprodcncf  46614  dvmptmulf  46651  dvnmptdivc  46652  dvnmul  46657  dvmptfprod  46659  stoweidlem3  46717  stoweidlem34  46748  stoweidlem42  46756  stoweidlem48  46762  fourierdlem112  46932  sge0lempt  47124  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0iunmpt  47132  sge0ltfirpmpt2  47140  sge0isummpt2  47146  sge0xaddlem2  47148  sge0xadd  47149  meadjiun  47180  voliunsge0lem  47186  meaiunincf  47197  meaiuninc3  47199  meaiininc  47201  hoimbl2  47379  vonhoire  47386  vonn0ioo2  47404  vonn0icc2  47406  salpreimagtlt  47444