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

Theorem chvarv 1958
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 1673 . 2  |-  F/ x ps
2 chvarv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
3 chvarv.2 . 2  |-  ph
41, 2, 3chvar 1957 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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590
This theorem is referenced by:  axext3  2425  axrep1  4404  axsep2  4414  isso2i  4673  tz6.12f  5708  dfac12lem2  8313  wunex2  8905  ltordlem  9865  iscatd2  14619  yoniso  15095  mrcmndind  15494  gsum2dlem2  16462  gsum2dOLD  16464  isdrngrd  16858  frlmphl  18206  frlmup1  18226  mdetralt  18414  mdetunilem9  18426  neiptoptop  18735  neiptopnei  18736  cnextcn  19639  cnextfres  19640  ustuqtop4  19819  dscmet  20165  nrmmetd  20167  rolle  21462  chscllem2  25041  esumcvg  26535  eulerpartlemgvv  26759  eulerpartlemn  26764  prodfdiv  27411  ftc1anclem7  28473  ftc1anc  28475  fdc  28641  fdc1  28642  iscringd  28799  ismrcd2  29035  fphpdo  29156  monotoddzzfi  29283  monotoddzz  29284  mendlmod  29550  stoweidlem43  29838  stoweidlem62  29857  numclwlk2lem2f1o  30698  bnj1326  32017
  Copyright terms: Public domain W3C validator