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

Theorem chvar 2249
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 217 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
41, 3spim 2241 . 2 (∀𝑥𝜑𝜓)
5 chvar.3 . 2 𝜑
64, 5mpg 1714 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by:  chvarvOLD  2251  csbhypf  3517  axrep2  4695  axrep3  4696  opelopabsb  4899  wfisg  5617  tfindes  6931  findes  6965  dfoprab4f  7094  dom2lem  7858  zfcndrep  9292  pwfseqlem4a  9339  pwfseqlem4  9340  uzind4s  11582  seqof2  12678  fproddivf  14505  fprodsplitf  14506  gsumcom2  18145  mdetralt2  20181  mdetunilem2  20185  ptcldmpt  21174  elmptrab  21387  isfildlem  21418  dvmptfsum  23486  dvfsumlem2  23538  lgamgulmlem2  24500  fmptcof2  28632  aciunf1lem  28637  esum2dlem  29274  fiunelros  29357  measiun  29401  bnj849  30042  bnj1014  30077  bnj1384  30147  bnj1489  30171  bnj1497  30175  setinds  30720  frinsg  30779  finxpreclem6  32192  ptrest  32361  poimirlem24  32386  poimirlem25  32387  poimirlem26  32388  fdc1  32495  fsumshftd  33038  fsumshftdOLD  33039  fphpd  36181  monotuz  36307  monotoddzz  36309  oddcomabszz  36310  setindtrs  36393  flcidc  36546  binomcxplemnotnn0  37360  fiiuncl  38042  disjf1  38147  disjinfi  38158  fsumclf  38416  fsumsplitf  38417  fsummulc1f  38418  fsumnncl  38421  fsumf1of  38424  fsumiunss  38425  fsumreclf  38426  fsumlessf  38427  fsumsermpt  38429  fmul01  38430  fmuldfeq  38433  fmul01lt1lem1  38434  fmul01lt1lem2  38435  fprodexp  38444  fprodabs2  38445  climmulf  38454  climexp  38455  climsuse  38458  climrecf  38459  climinff  38461  climaddf  38465  mullimc  38466  neglimc  38497  addlimc  38498  0ellimcdiv  38499  climsubmpt  38510  climreclf  38514  climeldmeqmpt  38518  climfveqmpt  38521  fnlimfvre  38524  fprodcncf  38570  dvmptmulf  38610  dvnmptdivc  38611  dvnmul  38616  dvmptfprod  38618  stoweidlem3  38679  stoweidlem34  38710  stoweidlem42  38718  stoweidlem48  38724  fourierdlem112  38894  sge0lempt  39086  sge0iunmptlemfi  39089  sge0iunmptlemre  39091  sge0iunmpt  39094  sge0ltfirpmpt2  39102  sge0isummpt2  39108  sge0xaddlem2  39110  sge0xadd  39111  meadjiun  39142  voliunsge0lem  39148  meaiininc  39160  hoimbl2  39338  vonhoire  39346  vonn0ioo2  39364  vonn0icc2  39366  salpreimagtlt  39399  smflimlem3  39442
  Copyright terms: Public domain W3C validator