MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chvar Structured version   Visualization version   GIF version

Theorem chvar 2298
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
StepHypRef Expression
1 chvar.1 . . 3 𝑥𝜓
2 chvar.2 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32biimpd 219 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
41, 3spim 2290 . 2 (∀𝑥𝜑𝜓)
5 chvar.3 . 2 𝜑
64, 5mpg 1764 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  chvarvOLD  2300  csbhypf  3585  axrep2  4806  axrep3  4807  opelopabsb  5014  wfisg  5753  tfindes  7104  findes  7138  dfoprab4f  7270  dom2lem  8037  zfcndrep  9474  pwfseqlem4a  9521  pwfseqlem4  9522  uzind4s  11786  seqof2  12899  fsumsplitf  14516  fproddivf  14762  fprodsplitf  14763  gsumcom2  18420  mdetralt2  20463  mdetunilem2  20467  ptcldmpt  21465  elmptrab  21678  isfildlem  21708  dvmptfsum  23783  dvfsumlem2  23835  lgamgulmlem2  24801  fmptcof2  29585  aciunf1lem  29590  fsumiunle  29703  esum2dlem  30282  fiunelros  30365  measiun  30409  bnj849  31121  bnj1014  31156  bnj1384  31226  bnj1489  31250  bnj1497  31254  setinds  31807  frpoinsg  31866  frinsg  31870  finxpreclem6  33363  ptrest  33538  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  fdc1  33672  fsumshftd  34556  fphpd  37697  monotuz  37823  monotoddzz  37825  oddcomabszz  37826  setindtrs  37909  flcidc  38061  binomcxplemnotnn0  38872  fiiuncl  39548  disjf1  39683  disjinfi  39694  supxrleubrnmptf  39993  monoordxr  40026  monoord2xr  40028  fsumclf  40119  fsummulc1f  40120  fsumnncl  40121  fsumf1of  40124  fsumiunss  40125  fsumreclf  40126  fsumlessf  40127  fsumsermpt  40129  fmul01  40130  fmuldfeq  40133  fmul01lt1lem1  40134  fmul01lt1lem2  40135  fprodexp  40144  fprodabs2  40145  climmulf  40154  climexp  40155  climsuse  40158  climrecf  40159  climinff  40161  climaddf  40165  mullimc  40166  neglimc  40197  addlimc  40198  0ellimcdiv  40199  climsubmpt  40210  climreclf  40214  climeldmeqmpt  40218  climfveqmpt  40221  fnlimfvre  40224  climfveqf  40230  climfveqmpt3  40232  climeldmeqf  40233  climeqf  40238  climeldmeqmpt3  40239  climinf2  40257  climinf2mpt  40264  climinfmpt  40265  limsupequz  40273  limsupequzmptf  40281  fprodcncf  40432  dvmptmulf  40470  dvnmptdivc  40471  dvnmul  40476  dvmptfprod  40478  stoweidlem3  40538  stoweidlem34  40569  stoweidlem42  40577  stoweidlem48  40583  fourierdlem112  40753  sge0lempt  40945  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  sge0ltfirpmpt2  40961  sge0isummpt2  40967  sge0xaddlem2  40969  sge0xadd  40970  meadjiun  41001  voliunsge0lem  41007  meaiunincf  41018  meaiuninc3  41020  meaiininc  41022  hoimbl2  41200  vonhoire  41207  vonn0ioo2  41225  vonn0icc2  41227  salpreimagtlt  41260  smflimlem3  41302
  Copyright terms: Public domain W3C validator