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

Theorem chvarv 2039
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 2024 . 2  |-  ( A. x ph  ->  ps )
3 chv.2 . 2  |-  ph
42, 3mpg 1554 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  axext3  2363  axrep1  4255  axsep2  4265  isso2i  4469  tz6.12f  5682  dfac12lem2  7950  wunex2  8539  ltordlem  9477  iscatd2  13826  yoniso  14302  gsum2d  15466  isdrngrd  15781  neiptoptop  17111  neiptopnei  17112  cnextcn  18012  cnextfres  18013  ustuqtop4  18188  dscmet  18484  nrmmetd  18486  rolle  19734  chscllem2  22981  esumcvg  24265  prodfdiv  24996  fdc  26133  fdc1  26134  iscringd  26293  ismrcd2  26437  fphpdo  26562  monotoddzzfi  26689  monotoddzz  26690  frlmup1  26912  mendlmod  27163  stoweidlem43  27453  stoweidlem62  27472  bnj1326  28726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator