MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chvarvv Structured version   Visualization version   GIF version

Theorem chvarvv 2003
Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2395 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 20-Apr-1994.) (Revised by BJ, 31-May-2019.)
Hypotheses
Ref Expression
chvarvv.1 (𝑥 = 𝑦 → (𝜑𝜓))
chvarvv.2 𝜑
Assertion
Ref Expression
chvarvv 𝜓
Distinct variable groups:   𝑥,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem chvarvv
StepHypRef Expression
1 chvarvv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21spvv 2001 . 2 (∀𝑥𝜑𝜓)
3 chvarvv.2 . 2 𝜑
42, 3mpg 1800 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  axextg  2710  nfcriOLD  2898  nfcriOLDOLD  2899  axrep1  5244  axsepg  5258  tz6.12f  6869  frrlem12  8229  dfac12lem2  10081  wunex2  10675  ltordlem  11681  prodfdiv  15782  iscatd2  17562  yoniso  18175  mndind  18639  gsum2dlem2  19749  isdrngrd  20216  isdrngrdOLD  20218  frlmphl  21190  frlmup1  21207  mdetralt  21960  mdetunilem9  21972  neiptoptop  22485  neiptopnei  22486  cnextcn  23421  cnextfres1  23422  ustuqtop4  23599  dscmet  23931  nrmmetd  23933  rolle  25357  numclwlk2lem2f1o  29326  chscllem2  30583  suppovss  31601  fedgmullem1  32327  esumcvg  32688  eulerpartlemgvv  32979  eulerpartlemn  32984  bnj1326  33641  fwddifnp1  34753  poimirlem13  36094  poimirlem14  36095  poimirlem25  36106  poimirlem31  36112  ftc1anclem7  36160  ftc1anc  36162  fdc  36207  fdc1  36208  iscringd  36460  sticksstones2  40558  ismrcd2  41025  fphpdo  41143  monotoddzzfi  41269  monotoddzz  41270  mendlmod  41523  dvgrat  42599  cvgdvgrat  42600  binomcxplemnotnn0  42643  iunincfi  43311  wessf1ornlem  43410  monoords  43538  limcperiod  43876  sumnnodd  43878  cncfshift  44122  cncfperiod  44127  icccncfext  44135  fperdvper  44167  dvnprodlem1  44194  dvnprodlem2  44195  dvnprodlem3  44196  iblspltprt  44221  itgspltprt  44227  stoweidlem43  44291  stoweidlem62  44310  dirkercncflem2  44352  fourierdlem12  44367  fourierdlem15  44370  fourierdlem34  44389  fourierdlem41  44396  fourierdlem42  44397  fourierdlem48  44402  fourierdlem50  44404  fourierdlem51  44405  fourierdlem73  44427  fourierdlem79  44433  fourierdlem81  44435  fourierdlem83  44437  fourierdlem92  44446  fourierdlem94  44448  fourierdlem103  44457  fourierdlem104  44458  fourierdlem111  44465  fourierdlem112  44466  fourierdlem113  44467  etransclem2  44484  etransclem46  44528  intsaluni  44577  meaiuninclem  44728  meaiuninc3v  44732  meaiininclem  44734  ovn0lem  44813  hoidmvlelem2  44844  hoidmvlelem3  44845  hspmbllem2  44875  vonioo  44930  vonicc  44933  pimincfltioc  44964  smflimlem3  45021  smflimlem4  45022
  Copyright terms: Public domain W3C validator