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

Theorem chvar 2260
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 2252 . 2 (∀𝑥𝜑𝜓)
5 chvar.3 . 2 𝜑
64, 5mpg 1722 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045  ax-13 2244
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708
This theorem is referenced by:  chvarvOLD  2262  csbhypf  3545  axrep2  4764  axrep3  4765  opelopabsb  4975  wfisg  5703  tfindes  7047  findes  7081  dfoprab4f  7211  dom2lem  7980  zfcndrep  9421  pwfseqlem4a  9468  pwfseqlem4  9469  uzind4s  11733  seqof2  12842  fsumsplitf  14453  fproddivf  14699  fprodsplitf  14700  gsumcom2  18355  mdetralt2  20396  mdetunilem2  20400  ptcldmpt  21398  elmptrab  21611  isfildlem  21642  dvmptfsum  23719  dvfsumlem2  23771  lgamgulmlem2  24737  fmptcof2  29430  aciunf1lem  29435  fsumiunle  29549  esum2dlem  30128  fiunelros  30211  measiun  30255  bnj849  30969  bnj1014  31004  bnj1384  31074  bnj1489  31098  bnj1497  31102  setinds  31657  frinsg  31716  finxpreclem6  33204  ptrest  33379  poimirlem24  33404  poimirlem25  33405  poimirlem26  33406  fdc1  33513  fsumshftd  34056  fsumshftdOLD  34057  fphpd  37199  monotuz  37325  monotoddzz  37327  oddcomabszz  37328  setindtrs  37411  flcidc  37563  binomcxplemnotnn0  38375  fiiuncl  39054  disjf1  39185  disjinfi  39196  supxrleubrnmptf  39493  fsumclf  39601  fsummulc1f  39602  fsumnncl  39603  fsumf1of  39606  fsumiunss  39607  fsumreclf  39608  fsumlessf  39609  fsumsermpt  39611  fmul01  39612  fmuldfeq  39615  fmul01lt1lem1  39616  fmul01lt1lem2  39617  fprodexp  39626  fprodabs2  39627  climmulf  39636  climexp  39637  climsuse  39640  climrecf  39641  climinff  39643  climaddf  39647  mullimc  39648  neglimc  39679  addlimc  39680  0ellimcdiv  39681  climsubmpt  39692  climreclf  39696  climeldmeqmpt  39700  climfveqmpt  39703  fnlimfvre  39706  climfveqf  39712  climfveqmpt3  39714  climeldmeqf  39715  climeqf  39720  climeldmeqmpt3  39721  climinf2  39739  climinf2mpt  39746  climinfmpt  39747  limsupequz  39755  limsupequzmptf  39763  fprodcncf  39877  dvmptmulf  39915  dvnmptdivc  39916  dvnmul  39921  dvmptfprod  39923  stoweidlem3  39983  stoweidlem34  40014  stoweidlem42  40022  stoweidlem48  40028  fourierdlem112  40198  sge0lempt  40390  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  sge0iunmpt  40398  sge0ltfirpmpt2  40406  sge0isummpt2  40412  sge0xaddlem2  40414  sge0xadd  40415  meadjiun  40446  voliunsge0lem  40452  meaiininc  40464  hoimbl2  40642  vonhoire  40649  vonn0ioo2  40667  vonn0icc2  40669  salpreimagtlt  40702  smflimlem3  40744
  Copyright terms: Public domain W3C validator