Theorem chvar 2250

Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.)

Hypotheses

Ref	Expression
chvar.1	⊢ Ⅎ𝑥𝜓
chvar.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
chvar.3	⊢ 𝜑

Assertion

Ref	Expression
chvar	⊢ 𝜓

Proof of Theorem chvar

Step	Hyp	Ref	Expression
1		chvar.1	. . 3 ⊢ Ⅎ𝑥𝜓
2		chvar.2	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpd 218	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spim 2242	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvar.3	. 2 ⊢ 𝜑
6	4, 5	mpg 1715	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701

This theorem is referenced by:  chvarvOLD  2252  csbhypf  3518  axrep2  4701  axrep3  4702  opelopabsb  4910  wfisg  5632  tfindes  6954  findes  6988  dfoprab4f  7117  dom2lem  7881  zfcndrep  9315  pwfseqlem4a  9362  pwfseqlem4  9363  uzind4s  11624  seqof2  12721  fproddivf  14557  fprodsplitf  14558  gsumcom2  18197  mdetralt2  20234  mdetunilem2  20238  ptcldmpt  21227  elmptrab  21440  isfildlem  21471  dvmptfsum  23542  dvfsumlem2  23594  lgamgulmlem2  24556  fmptcof2  28839  aciunf1lem  28844  esum2dlem  29481  fiunelros  29564  measiun  29608  bnj849  30249  bnj1014  30284  bnj1384  30354  bnj1489  30378  bnj1497  30382  setinds  30927  frinsg  30986  finxpreclem6  32409  ptrest  32578  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  fdc1  32712  fsumshftd  33255  fsumshftdOLD  33256  fphpd  36398  monotuz  36524  monotoddzz  36526  oddcomabszz  36527  setindtrs  36610  flcidc  36763  binomcxplemnotnn0  37577  fiiuncl  38259  disjf1  38364  disjinfi  38375  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  fsumnncl  38638  fsumf1of  38641  fsumiunss  38642  fsumreclf  38643  fsumlessf  38644  fsumsermpt  38646  fmul01  38647  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodexp  38661  fprodabs2  38662  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climinff  38678  climaddf  38682  mullimc  38683  neglimc  38714  addlimc  38715  0ellimcdiv  38716  climsubmpt  38727  climreclf  38731  climeldmeqmpt  38735  climfveqmpt  38738  fnlimfvre  38741  fprodcncf  38787  dvmptmulf  38827  dvnmptdivc  38828  dvnmul  38833  dvmptfprod  38835  stoweidlem3  38896  stoweidlem34  38927  stoweidlem42  38935  stoweidlem48  38941  fourierdlem112  39111  sge0lempt  39303  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isummpt2  39325  sge0xaddlem2  39327  sge0xadd  39328  meadjiun  39359  voliunsge0lem  39365  meaiininc  39377  hoimbl2  39555  vonhoire  39563  vonn0ioo2  39581  vonn0icc2  39583  salpreimagtlt  39616  smflimlem3  39659