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

Theorem chvarv 1970
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 1674 . 2
2 chvarv.1 . 2
3 chvarv.2 . 2
41, 2, 3chvar 1969 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  axext3OLD  2435  axrep1  4521  axsep2  4531  isso2i  4790  tz6.12f  5831  dfac12lem2  8450  wunex2  9042  ltordlem  10002  iscatd2  14778  yoniso  15254  mrcmndind  15653  gsum2dlem2  16631  gsum2dOLD  16633  isdrngrd  17034  frlmphl  18399  frlmup1  18419  mdetralt  18682  mdetunilem9  18694  neiptoptop  19134  neiptopnei  19135  cnextcn  20038  cnextfres  20039  ustuqtop4  20218  dscmet  20564  nrmmetd  20566  rolle  21862  chscllem2  25510  esumcvg  26992  eulerpartlemgvv  27215  eulerpartlemn  27220  prodfdiv  27867  ftc1anclem7  28933  ftc1anc  28935  fdc  29101  fdc1  29102  iscringd  29259  ismrcd2  29495  fphpdo  29616  monotoddzzfi  29743  monotoddzz  29744  mendlmod  30010  sumnnodd  30401  fperdvper  30477  stoweidlem43  30572  stoweidlem62  30591  fourierdlem41  30677  fourierdlem48  30684  fourierdlem51  30687  fourierdlem83  30719  fourierdlem94  30730  fourierdlem111  30747  fourierdlem112  30748  fourierdlem113  30749  numclwlk2lem2f1o  31575  bnj1326  32860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1955
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
  Copyright terms: Public domain W3C validator