Theorem chvar 2369

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 230	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	spim 2361	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
5		chvar.3	. 2 ⊢ 𝜑
6	4, 5	mpg 1779	1 ⊢ 𝜓

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-12 2141  ax-13 2344

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-nf 1766

This theorem is referenced by:  chvarv  2370  csbhypf  3836  opelopabsb  5307  wfisg  6058  tfindes  7433  findes  7468  dfoprab4f  7610  dom2lem  8397  zfcndrep  9882  pwfseqlem4a  9929  pwfseqlem4  9930  uzind4s  12157  seqof2  13278  fsumsplitf  14931  fproddivf  15174  fprodsplitf  15175  gsumcom2  18815  mdetralt2  20902  mdetunilem2  20906  ptcldmpt  21906  elmptrab  22119  isfildlem  22149  dvmptfsum  24255  dvfsumlem2  24307  lgamgulmlem2  25289  fmptcof2  30092  aciunf1lem  30097  fsumiunle  30229  esum2dlem  30968  fiunelros  31050  measiun  31094  bnj849  31813  bnj1014  31848  bnj1384  31918  bnj1489  31942  bnj1497  31946  setinds  32631  frpoinsg  32690  frinsg  32696  finxpreclem6  34208  ptrest  34422  poimirlem24  34447  poimirlem25  34448  poimirlem26  34449  fdc1  34553  fsumshftd  35619  fphpd  38898  monotuz  39023  monotoddzz  39025  oddcomabszz  39026  setindtrs  39107  flcidc  39259  binomcxplemnotnn0  40226  fiiuncl  40866  disjf1  40983  disjinfi  40994  supxrleubrnmptf  41269  monoordxr  41301  monoord2xr  41303  fsumclf  41392  fsummulc1f  41393  fsumnncl  41394  fsumf1of  41397  fsumiunss  41398  fsumreclf  41399  fsumlessf  41400  fsumsermpt  41402  fmul01  41403  fmuldfeq  41406  fmul01lt1lem1  41407  fmul01lt1lem2  41408  fprodexp  41417  fprodabs2  41418  climmulf  41427  climexp  41428  climsuse  41431  climrecf  41432  climinff  41434  climaddf  41438  mullimc  41439  neglimc  41470  addlimc  41471  0ellimcdiv  41472  climsubmpt  41483  climreclf  41487  climeldmeqmpt  41491  climfveqmpt  41494  fnlimfvre  41497  climfveqf  41503  climfveqmpt3  41505  climeldmeqf  41506  climeqf  41511  climeldmeqmpt3  41512  climinf2  41530  climinf2mpt  41537  climinfmpt  41538  limsupequz  41546  limsupequzmptf  41554  fprodcncf  41725  dvmptmulf  41763  dvnmptdivc  41764  dvnmul  41769  dvmptfprod  41771  stoweidlem3  41830  stoweidlem34  41861  stoweidlem42  41869  stoweidlem48  41875  fourierdlem112  42045  sge0lempt  42234  sge0iunmptlemfi  42237  sge0iunmptlemre  42239  sge0iunmpt  42242  sge0ltfirpmpt2  42250  sge0isummpt2  42256  sge0xaddlem2  42258  sge0xadd  42259  meadjiun  42290  voliunsge0lem  42296  meaiunincf  42307  meaiuninc3  42309  meaiininc  42311  hoimbl2  42489  vonhoire  42496  vonn0ioo2  42514  vonn0icc2  42516  salpreimagtlt  42549  smflimlem3  42591