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

Theorem chvar 2408
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 2400 . 2 (∀𝑥𝜑𝜓)
5 chvar.3 . 2 𝜑
64, 5mpg 1873 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-12 2197  ax-13 2392
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-nf 1859
This theorem is referenced by:  chvarvOLD  2410  csbhypf  3694  axrep2  4926  axrep3  4927  opelopabsb  5136  wfisg  5877  tfindes  7229  findes  7263  dfoprab4f  7395  dom2lem  8164  zfcndrep  9649  pwfseqlem4a  9696  pwfseqlem4  9697  uzind4s  11962  seqof2  13074  fsumsplitf  14692  fproddivf  14938  fprodsplitf  14939  gsumcom2  18595  mdetralt2  20638  mdetunilem2  20642  ptcldmpt  21640  elmptrab  21853  isfildlem  21883  dvmptfsum  23958  dvfsumlem2  24010  lgamgulmlem2  24977  fmptcof2  29788  aciunf1lem  29793  fsumiunle  29906  esum2dlem  30485  fiunelros  30568  measiun  30612  bnj849  31324  bnj1014  31359  bnj1384  31429  bnj1489  31453  bnj1497  31457  setinds  32010  frpoinsg  32069  frinsg  32073  finxpreclem6  33563  ptrest  33740  poimirlem24  33765  poimirlem25  33766  poimirlem26  33767  fdc1  33874  fsumshftd  34760  fphpd  37901  monotuz  38027  monotoddzz  38029  oddcomabszz  38030  setindtrs  38113  flcidc  38265  binomcxplemnotnn0  39076  fiiuncl  39752  disjf1  39887  disjinfi  39898  supxrleubrnmptf  40197  monoordxr  40230  monoord2xr  40232  fsumclf  40323  fsummulc1f  40324  fsumnncl  40325  fsumf1of  40328  fsumiunss  40329  fsumreclf  40330  fsumlessf  40331  fsumsermpt  40333  fmul01  40334  fmuldfeq  40337  fmul01lt1lem1  40338  fmul01lt1lem2  40339  fprodexp  40348  fprodabs2  40349  climmulf  40358  climexp  40359  climsuse  40362  climrecf  40363  climinff  40365  climaddf  40369  mullimc  40370  neglimc  40401  addlimc  40402  0ellimcdiv  40403  climsubmpt  40414  climreclf  40418  climeldmeqmpt  40422  climfveqmpt  40425  fnlimfvre  40428  climfveqf  40434  climfveqmpt3  40436  climeldmeqf  40437  climeqf  40442  climeldmeqmpt3  40443  climinf2  40461  climinf2mpt  40468  climinfmpt  40469  limsupequz  40477  limsupequzmptf  40485  fprodcncf  40636  dvmptmulf  40674  dvnmptdivc  40675  dvnmul  40680  dvmptfprod  40682  stoweidlem3  40742  stoweidlem34  40773  stoweidlem42  40781  stoweidlem48  40787  fourierdlem112  40957  sge0lempt  41149  sge0iunmptlemfi  41152  sge0iunmptlemre  41154  sge0iunmpt  41157  sge0ltfirpmpt2  41165  sge0isummpt2  41171  sge0xaddlem2  41173  sge0xadd  41174  meadjiun  41205  voliunsge0lem  41211  meaiunincf  41222  meaiuninc3  41224  meaiininc  41226  hoimbl2  41404  vonhoire  41411  vonn0ioo2  41429  vonn0icc2  41431  salpreimagtlt  41464  smflimlem3  41506
  Copyright terms: Public domain W3C validator