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

Theorem chvarv 1966
Description: Implicit substitution of  y for  x into a theorem. (Contributed by NM, 20-Apr-1994.)
Hypotheses
Ref Expression
chv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
chv.2  |-  ph
Assertion
Ref Expression
chvarv  |-  ps
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x, y)    ps( y)

Proof of Theorem chvarv
StepHypRef Expression
1 chv.1 . . 3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
21spv 1951 . 2  |-  ( A. x ph  ->  ps )
3 chv.2 . 2  |-  ph
42, 3mpg 1538 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  axext3  2279  axrep1  4148  axsep2  4158  isso2i  4362  tz6.12f  5562  dfac12lem2  7786  wunex2  8376  ltordlem  9314  iscatd2  13599  yoniso  14075  gsum2d  15239  isdrngrd  15554  dscmet  18111  nrmmetd  18113  rolle  19353  chscllem2  22233  esumcvg  23469  inposet  25381  fdc  26558  fdc1  26559  iscringd  26727  ismrcd2  26877  fphpdo  27003  monotoddzzfi  27130  monotoddzz  27131  frlmup1  27353  mendlmod  27604  bnj1326  29372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator