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

Theorem chvar 2013
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 207 . . 3
41, 3spim 2006 . 2
5 chvar.3 . 2
64, 5mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616
This theorem is referenced by:  chvarv  2014  csbhypf  3453  axrep2  4565  axrep3  4566  opelopabsb  4762  tfindes  6697  findes  6730  dfoprab4f  6858  dom2lem  7575  zfcndrep  9013  pwfseqlem4a  9060  pwfseqlem4  9061  uzind4s  11170  seqof2  12165  gsumcom2  17003  mdetralt2  19111  mdetunilem2  19115  ptcldmpt  20115  elmptrab  20328  isfildlem  20358  dvmptfsum  22376  dvfsumlem2  22428  fmptcof2  27502  measiun  28189  lgamgulmlem2  28572  setinds  29210  wfisg  29289  frinsg  29325  ptrest  30048  fdc1  30239  fphpd  30750  monotuz  30877  monotoddzz  30879  oddcomabszz  30880  setindtrs  30967  flcidc  31123  binomcxplemnotnn0  31261  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumnncl  31572  fmul01  31574  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fproddivf  31588  fprodsplitf  31589  fprodexp  31600  fprodabs2  31602  climmulf  31610  climexp  31611  climsuse  31614  climrecf  31615  climinff  31617  climaddf  31621  mullimc  31622  neglimc  31653  addlimc  31654  0ellimcdiv  31655  fprodcncf  31704  dvmptmulf  31734  dvnmptdivc  31735  dvnmul  31740  dvmptfprod  31742  stoweidlem3  31785  stoweidlem34  31816  stoweidlem42  31824  stoweidlem48  31830  fourierdlem112  32001  bnj849  33983  bnj1014  34018  bnj1384  34088  bnj1489  34112  bnj1497  34116  fsumshftd  34682  fsumshftdOLD  34683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator