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

Theorem chvarv 1969
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
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 nfv 1629 . 2  |-  F/ x ps
2 chv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
3 chv.2 . 2  |-  ph
41, 2, 3chvar 1968 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  axext3  2418  axrep1  4313  axsep2  4323  isso2i  4527  tz6.12f  5741  dfac12lem2  8016  wunex2  8605  ltordlem  9544  iscatd2  13898  yoniso  14374  gsum2d  15538  isdrngrd  15853  neiptoptop  17187  neiptopnei  17188  cnextcn  18090  cnextfres  18091  ustuqtop4  18266  dscmet  18612  nrmmetd  18614  rolle  19866  chscllem2  23132  esumcvg  24468  prodfdiv  25216  ftc1anclem7  26276  ftc1anc  26278  fdc  26440  fdc1  26441  iscringd  26600  ismrcd2  26744  fphpdo  26869  monotoddzzfi  26996  monotoddzz  26997  frlmup1  27218  mendlmod  27469  stoweidlem43  27759  stoweidlem62  27778  bnj1326  29332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator