Theorem chvarv 2263

Description: Implicit substitution of y for x into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 14-Jul-2021.)

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

Step	Hyp	Ref	Expression
1		chvarv.1	. . 3 |- ( x = y -> ( ph <-> ps ) )
2	1	spv 2260	. 2 |- ( A. x ph -> ps )
3		chvarv.2	. 2 |- ph
4	2, 3	mpg 1724	1 |- ps

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  axext3ALT  2605  axrep1  4772  axsep2  4782  isso2i  5067  tz6.12f  6212  dfac12lem2  8966  wunex2  9560  ltordlem  10553  prodfdiv  14628  iscatd2  16342  yoniso  16925  mrcmndind  17366  gsum2dlem2  18370  isdrngrd  18773  frlmphl  20120  frlmup1  20137  mdetralt  20414  mdetunilem9  20426  neiptoptop  20935  neiptopnei  20936  cnextcn  21871  cnextfres1  21872  ustuqtop4  22048  dscmet  22377  nrmmetd  22379  rolle  23753  numclwlk2lem2f1o  27238  chscllem2  28497  esumcvg  30148  eulerpartlemgvv  30438  eulerpartlemn  30443  bnj1326  31094  fwddifnp1  32272  poimirlem13  33422  poimirlem14  33423  poimirlem25  33434  poimirlem31  33440  ftc1anclem7  33491  ftc1anc  33493  fdc  33541  fdc1  33542  iscringd  33797  ismrcd2  37262  fphpdo  37381  monotoddzzfi  37507  monotoddzz  37508  mendlmod  37763  dvgrat  38511  cvgdvgrat  38512  binomcxplemnotnn0  38555  iunincfi  39272  wessf1ornlem  39371  monoords  39511  limcperiod  39860  sumnnodd  39862  cncfshift  40087  cncfperiod  40092  icccncfext  40100  fperdvper  40133  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  iblspltprt  40189  itgspltprt  40195  stoweidlem43  40260  stoweidlem62  40279  dirkercncflem2  40321  fourierdlem12  40336  fourierdlem15  40339  fourierdlem34  40358  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem50  40373  fourierdlem51  40374  fourierdlem73  40396  fourierdlem79  40402  fourierdlem81  40404  fourierdlem83  40406  fourierdlem92  40415  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  etransclem2  40453  etransclem46  40497  intsaluni  40547  meaiuninclem  40697  meaiininclem  40700  ovn0lem  40779  hoidmvlelem2  40810  hoidmvlelem3  40811  hspmbllem2  40841  vonioo  40896  vonicc  40899  pimincfltioc  40926  smflimlem4  40982