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

Theorem chvar 2438
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 220 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
41, 3spim 2430 . 2 (∀𝑥𝜑𝜓)
5 chvar.3 . 2 𝜑
64, 5mpg 1879 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-12 2215  ax-13 2422
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-nf 1864
This theorem is referenced by:  chvarv  2439  csbhypf  3758  axrep2  4980  axrep3  4981  opelopabsb  5193  wfisg  5941  tfindes  7301  findes  7335  dfoprab4f  7467  dom2lem  8241  zfcndrep  9730  pwfseqlem4a  9777  pwfseqlem4  9778  uzind4s  11985  seqof2  13101  fsumsplitf  14714  fproddivf  14957  fprodsplitf  14958  gsumcom2  18594  mdetralt2  20646  mdetunilem2  20650  ptcldmpt  21651  elmptrab  21864  isfildlem  21894  dvmptfsum  23974  dvfsumlem2  24026  lgamgulmlem2  24992  fmptcof2  29806  aciunf1lem  29811  fsumiunle  29924  esum2dlem  30501  fiunelros  30584  measiun  30628  bnj849  31339  bnj1014  31374  bnj1384  31444  bnj1489  31468  bnj1497  31472  setinds  32024  frpoinsg  32083  frinsg  32087  finxpreclem6  33567  ptrest  33739  poimirlem24  33764  poimirlem25  33765  poimirlem26  33766  fdc1  33871  fsumshftd  34749  fphpd  37899  monotuz  38024  monotoddzz  38026  oddcomabszz  38027  setindtrs  38110  flcidc  38262  binomcxplemnotnn0  39072  fiiuncl  39744  disjf1  39875  disjinfi  39886  supxrleubrnmptf  40176  monoordxr  40209  monoord2xr  40211  fsumclf  40298  fsummulc1f  40299  fsumnncl  40300  fsumf1of  40303  fsumiunss  40304  fsumreclf  40305  fsumlessf  40306  fsumsermpt  40308  fmul01  40309  fmuldfeq  40312  fmul01lt1lem1  40313  fmul01lt1lem2  40314  fprodexp  40323  fprodabs2  40324  climmulf  40333  climexp  40334  climsuse  40337  climrecf  40338  climinff  40340  climaddf  40344  mullimc  40345  neglimc  40376  addlimc  40377  0ellimcdiv  40378  climsubmpt  40389  climreclf  40393  climeldmeqmpt  40397  climfveqmpt  40400  fnlimfvre  40403  climfveqf  40409  climfveqmpt3  40411  climeldmeqf  40412  climeqf  40417  climeldmeqmpt3  40418  climinf2  40436  climinf2mpt  40443  climinfmpt  40444  limsupequz  40452  limsupequzmptf  40460  fprodcncf  40611  dvmptmulf  40649  dvnmptdivc  40650  dvnmul  40655  dvmptfprod  40657  stoweidlem3  40716  stoweidlem34  40747  stoweidlem42  40755  stoweidlem48  40761  fourierdlem112  40931  sge0lempt  41123  sge0iunmptlemfi  41126  sge0iunmptlemre  41128  sge0iunmpt  41131  sge0ltfirpmpt2  41139  sge0isummpt2  41145  sge0xaddlem2  41147  sge0xadd  41148  meadjiun  41179  voliunsge0lem  41185  meaiunincf  41196  meaiuninc3  41198  meaiininc  41200  hoimbl2  41378  vonhoire  41385  vonn0ioo2  41403  vonn0icc2  41405  salpreimagtlt  41438  smflimlem3  41480
  Copyright terms: Public domain W3C validator