Theorem chvarfv 2280

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 2279	. 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 1945  ax-6 2002  ax-7 2043  ax-12 2216

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

This theorem is used by:  csbhypf  3879  axrep2  5241  axrep3  5242  isso2i  5603  frpoinsg  6372  tfindes  7908  findes  7946  dfoprab4f  8102  dom2lem  9057  setinds  9787  frinsg  9792  pwfseqlem4a  10785  pwfseqlem4  10786  uzind4s  13075  seqof2  14243  fsumclf  15948  fsumsplitf  15952  fproddivf  16198  fprodsplitf  16199  gsumcom2  20240  mdetralt2  22979  mdetunilem2  22983  ptcldmpt  23988  elmptrab  24201  isfildlem  24231  dvmptfsum  26350  dvfsumlem2  26402  lgamgulmlem2  27414  fmptcof2  33349  aciunf1lem  33354  fsumiunle  33516  esum2dlem  34835  fiunelros  34918  measiun  34962  bnj849  35666  bnj1014  35702  bnj1384  35773  bnj1489  35797  bnj1497  35801  finxpreclem6  38587  ptrest  38805  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  fdc1  38946  fsumshftd  40275  fphpd  44089  monotuz  44214  monotoddzz  44216  oddcomabszz  44217  setindtrs  44298  flcidc  44433  binomcxplemnotnn0  45601  fiiuncl  46356  disjf1  46471  disjinfi  46480  supxrleubrnmptf  46734  monoordxr  46765  monoord2xr  46767  fsummulc1f  46856  fsumnncl  46857  fsumf1of  46859  fsumiunss  46860  fsumreclf  46861  fsumlessf  46862  fsumsermpt  46864  fmul01  46865  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  fprodexp  46879  fprodabs2  46880  climmulf  46889  climexp  46890  climsuse  46893  climrecf  46894  climinff  46896  climaddf  46900  mullimc  46901  neglimc  46930  addlimc  46931  0ellimcdiv  46932  climsubmpt  46943  climreclf  46947  climeldmeqmpt  46951  climfveqmpt  46954  fnlimfvre  46957  climfveqf  46963  climfveqmpt3  46965  climeldmeqf  46966  climeqf  46971  climeldmeqmpt3  46972  climinf2  46990  climinf2mpt  46997  climinfmpt  46998  limsupequz  47006  limsupequzmptf  47014  fprodcncf  47183  dvmptmulf  47220  dvnmptdivc  47221  dvnmul  47226  dvmptfprod  47228  stoweidlem3  47286  stoweidlem34  47317  stoweidlem42  47325  stoweidlem48  47331  fourierdlem112  47501  sge0lempt  47693  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0iunmpt  47701  sge0ltfirpmpt2  47709  sge0isummpt2  47715  sge0xaddlem2  47717  sge0xadd  47718  meadjiun  47749  voliunsge0lem  47755  meaiunincf  47766  meaiuninc3  47768  meaiininc  47770  hoimbl2  47948  vonhoire  47955  vonn0ioo2  47973  vonn0icc2  47975  salpreimagtlt  48013