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

Theorem chvarv 1959
Description: Implicit substitution of  y for  x into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
Hypotheses
Ref Expression
chvarv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
chvarv.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 nfv 1674 . 2  |-  F/ x ps
2 chvarv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
3 chvarv.2 . 2  |-  ph
41, 2, 3chvar 1958 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-12 1793  ax-13 1944
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  axext3  2418  axrep1  4394  axsep2  4404  isso2i  4662  tz6.12f  5698  dfac12lem2  8303  wunex2  8895  ltordlem  9855  iscatd2  14604  yoniso  15080  mrcmndind  15478  gsum2dlem2  16438  gsum2dOLD  16440  isdrngrd  16784  frlmphl  18050  frlmup1  18070  mdetralt  18258  mdetunilem9  18270  neiptoptop  18579  neiptopnei  18580  cnextcn  19483  cnextfres  19484  ustuqtop4  19663  dscmet  20009  nrmmetd  20011  rolle  21306  chscllem2  24866  esumcvg  26391  eulerpartlemgvv  26609  eulerpartlemn  26614  prodfdiv  27260  ftc1anclem7  28319  ftc1anc  28321  fdc  28487  fdc1  28488  iscringd  28645  ismrcd2  28882  fphpdo  29003  monotoddzzfi  29130  monotoddzz  29131  mendlmod  29397  stoweidlem43  29686  stoweidlem62  29705  numclwlk2lem2f1o  30546  bnj1326  31759
  Copyright terms: Public domain W3C validator