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

Theorem chvarv 1949
Description: Implicit substitution of for into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
Hypotheses
Ref Expression
chvarv.1
chvarv.2
Assertion
Ref Expression
chvarv
Distinct variable group:   ,

Proof of Theorem chvarv
StepHypRef Expression
1 nfv 1664 . 2
2 chvarv.1 . 2
3 chvarv.2 . 2
41, 2, 3chvar 1948 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  axext3  2405  axrep1  4379  axsep2  4389  isso2i  4644  tz6.12f  5678  dfac12lem2  8260  wunex2  8851  ltordlem  9811  iscatd2  14559  yoniso  15035  mrcmndind  15433  gsum2d  16355  isdrngrd  16671  frlmup1  17926  mdetralt  18116  mdetunilem9  18128  neiptoptop  18439  neiptopnei  18440  cnextcn  19343  cnextfres  19344  ustuqtop4  19519  dscmet  19865  nrmmetd  19867  rolle  21162  chscllem2  24720  esumcvg  26244  eulerpartlemgvv  26462  eulerpartlemn  26467  prodfdiv  27113  ftc1anclem7  28144  ftc1anc  28146  fdc  28312  fdc1  28313  iscringd  28470  ismrcd2  28707  fphpdo  28829  monotoddzzfi  28956  monotoddzz  28957  mendlmod  29223  stoweidlem43  29512  stoweidlem62  29531  numclwlk2lem2f1o  30372  gsumX2dlem2  30503  bnj1326  31595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-12 1785  ax-13 1934
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-nf 1585
  Copyright terms: Public domain W3C validator