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

Theorem chvarvv 2005
Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvarv 2414 with a disjoint variable condition, which does not require ax-13 2390. (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 2003 . 2 (∀𝑥𝜑𝜓)
3 chvarvv.2 . 2 𝜑
42, 3mpg 1798 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970
This theorem depends on definitions:  df-bi 209  df-ex 1781
This theorem is referenced by:  axextg  2794  axrep1  5163  axsepg  5176  tz6.12f  6666  dfac12lem2  9544  wunex2  10134  ltordlem  11139  prodfdiv  15228  iscatd2  16927  yoniso  17510  mndind  17967  gsum2dlem2  19066  isdrngrd  19500  frlmphl  20897  frlmup1  20914  mdetralt  21189  mdetunilem9  21201  neiptoptop  21711  neiptopnei  21712  cnextcn  22647  cnextfres1  22648  ustuqtop4  22825  dscmet  23154  nrmmetd  23156  rolle  24568  numclwlk2lem2f1o  28139  chscllem2  29396  suppovss  30409  fedgmullem1  31032  esumcvg  31349  eulerpartlemgvv  31638  eulerpartlemn  31643  bnj1326  32302  frrlem12  33138  fwddifnp1  33630  poimirlem13  34942  poimirlem14  34943  poimirlem25  34954  poimirlem31  34960  ftc1anclem7  35008  ftc1anc  35010  fdc  35055  fdc1  35056  iscringd  35308  ismrcd2  39429  fphpdo  39547  monotoddzzfi  39672  monotoddzz  39673  mendlmod  39926  dvgrat  40795  cvgdvgrat  40796  binomcxplemnotnn0  40839  iunincfi  41511  wessf1ornlem  41595  monoords  41714  limcperiod  42057  sumnnodd  42059  cncfshift  42303  cncfperiod  42308  icccncfext  42316  fperdvper  42348  dvnprodlem1  42375  dvnprodlem2  42376  dvnprodlem3  42377  iblspltprt  42402  itgspltprt  42408  stoweidlem43  42472  stoweidlem62  42491  dirkercncflem2  42533  fourierdlem12  42548  fourierdlem15  42551  fourierdlem34  42570  fourierdlem41  42577  fourierdlem42  42578  fourierdlem48  42583  fourierdlem50  42585  fourierdlem51  42586  fourierdlem73  42608  fourierdlem79  42614  fourierdlem81  42616  fourierdlem83  42618  fourierdlem92  42627  fourierdlem94  42629  fourierdlem103  42638  fourierdlem104  42639  fourierdlem111  42646  fourierdlem112  42647  fourierdlem113  42648  etransclem2  42665  etransclem46  42709  intsaluni  42756  meaiuninclem  42906  meaiuninc3v  42910  meaiininclem  42912  ovn0lem  42991  hoidmvlelem2  43022  hoidmvlelem3  43023  hspmbllem2  43053  vonioo  43108  vonicc  43111  pimincfltioc  43138  smflimlem3  43193  smflimlem4  43194
  Copyright terms: Public domain W3C validator