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

Theorem chvarv 1953
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 1938 . 2  |-  ( A. x ph  ->  ps )
3 chv.2 . 2  |-  ph
42, 3mpg 1535 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  axext3  2266  axrep1  4132  axsep2  4142  isso2i  4346  tz6.12f  5546  dfac12lem2  7770  wunex2  8360  ltordlem  9298  iscatd2  13583  yoniso  14059  gsum2d  15223  isdrngrd  15538  dscmet  18095  nrmmetd  18097  rolle  19337  chscllem2  22217  esumcvg  23454  inposet  25278  fdc  26455  fdc1  26456  iscringd  26624  ismrcd2  26774  fphpdo  26900  monotoddzzfi  27027  monotoddzz  27028  frlmup1  27250  mendlmod  27501  bnj1326  29056
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator