Theorem chvarfv 2228

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  csbhypf  3918  axrep2  5289  axrep3  5290  isso2i  5625  frpoinsg  6351  wfisgOLD  6362  tfindes  7868  findes  7908  dfoprab4f  8061  dom2lem  9013  frinsg  9776  pwfseqlem4a  10686  pwfseqlem4  10687  uzind4s  12925  seqof2  14061  fsumclf  15720  fsumsplitf  15724  fproddivf  15967  fprodsplitf  15968  gsumcom2  19942  mdetralt2  22555  mdetunilem2  22559  ptcldmpt  23562  elmptrab  23775  isfildlem  23805  dvmptfsum  25951  dvfsumlem2  26005  dvfsumlem2OLD  26006  lgamgulmlem2  27007  fmptcof2  32524  aciunf1lem  32529  fsumiunle  32677  esum2dlem  33839  fiunelros  33921  measiun  33965  bnj849  34684  bnj1014  34720  bnj1384  34791  bnj1489  34815  bnj1497  34819  setinds  35502  finxpreclem6  37003  ptrest  37220  poimirlem24  37245  poimirlem25  37246  poimirlem26  37247  fdc1  37347  fsumshftd  38551  fphpd  42375  monotuz  42501  monotoddzz  42503  oddcomabszz  42504  setindtrs  42585  flcidc  42737  binomcxplemnotnn0  43932  fiiuncl  44568  disjf1  44692  disjinfi  44701  supxrleubrnmptf  44968  monoordxr  45000  monoord2xr  45002  fsummulc1f  45094  fsumnncl  45095  fsumf1of  45097  fsumiunss  45098  fsumreclf  45099  fsumlessf  45100  fsumsermpt  45102  fmul01  45103  fmuldfeq  45106  fmul01lt1lem1  45107  fmul01lt1lem2  45108  fprodexp  45117  fprodabs2  45118  climmulf  45127  climexp  45128  climsuse  45131  climrecf  45132  climinff  45134  climaddf  45138  mullimc  45139  neglimc  45170  addlimc  45171  0ellimcdiv  45172  climsubmpt  45183  climreclf  45187  climeldmeqmpt  45191  climfveqmpt  45194  fnlimfvre  45197  climfveqf  45203  climfveqmpt3  45205  climeldmeqf  45206  climeqf  45211  climeldmeqmpt3  45212  climinf2  45230  climinf2mpt  45237  climinfmpt  45238  limsupequz  45246  limsupequzmptf  45254  fprodcncf  45423  dvmptmulf  45460  dvnmptdivc  45461  dvnmul  45466  dvmptfprod  45468  stoweidlem3  45526  stoweidlem34  45557  stoweidlem42  45565  stoweidlem48  45571  fourierdlem112  45741  sge0lempt  45933  sge0iunmptlemfi  45936  sge0iunmptlemre  45938  sge0iunmpt  45941  sge0ltfirpmpt2  45949  sge0isummpt2  45955  sge0xaddlem2  45957  sge0xadd  45958  meadjiun  45989  voliunsge0lem  45995  meaiunincf  46006  meaiuninc3  46008  meaiininc  46010  hoimbl2  46188  vonhoire  46195  vonn0ioo2  46213  vonn0icc2  46215  salpreimagtlt  46253