Theorem chvarv 2014

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

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		chvarv.1	. 2
3		chvarv.2	. 2
4	1, 2, 3	chvar 2013	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  axext3OLD  2438  axrep1  4564  axsep2  4574  isso2i  4837  tz6.12f  5889  dfac12lem2  8545  wunex2  9137  ltordlem  10103  prodfdiv  13705  iscatd2  15078  yoniso  15554  mrcmndind  15997  gsum2dlem2  16998  gsum2dOLD  17000  isdrngrd  17422  frlmphl  18812  frlmup1  18832  mdetralt  19110  mdetunilem9  19122  neiptoptop  19632  neiptopnei  19633  cnextcn  20567  cnextfres  20568  ustuqtop4  20747  dscmet  21093  nrmmetd  21095  rolle  22391  numclwlk2lem2f1o  25105  chscllem2  26556  esumcvg  28092  eulerpartlemgvv  28315  eulerpartlemn  28320  ftc1anclem7  30096  ftc1anc  30098  fdc  30238  fdc1  30239  iscringd  30396  ismrcd2  30631  fphpdo  30751  monotoddzzfi  30878  monotoddzz  30879  mendlmod  31142  dvgrat  31193  cvgdvgrat  31194  binomcxplemnotnn0  31261  monoords  31496  limcperiod  31634  sumnnodd  31636  cncfshift  31676  cncfperiod  31681  icccncfext  31690  fperdvper  31715  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  iblspltprt  31772  itgspltprt  31778  stoweidlem43  31825  stoweidlem62  31844  dirkercncflem2  31886  fourierdlem12  31901  fourierdlem15  31904  fourierdlem34  31923  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem50  31939  fourierdlem51  31940  fourierdlem73  31962  fourierdlem79  31968  fourierdlem81  31970  fourierdlem83  31972  fourierdlem92  31981  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  etransclem2  32019  etransclem46  32063  bnj1326  34082

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