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

Theorem chvarv 2409
Description: Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) Remove dependency on ax-10 2169. (Revised by Wolf Lammen, 14-Jul-2021.)
Hypotheses
Ref Expression
chvarv.1 (𝑥 = 𝑦 → (𝜑𝜓))
chvarv.2 𝜑
Assertion
Ref Expression
chvarv 𝜓
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem chvarv
StepHypRef Expression
1 chvarv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21spv 2406 . 2 (∀𝑥𝜑𝜓)
3 chvarv.2 . 2 𝜑
42, 3mpg 1873 1 𝜓
Colors of variables: wff setvar class
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 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-12 2197  ax-13 2392
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854
This theorem is referenced by:  axext3ALT  2744  axrep1  4925  axsep2  4935  isso2i  5220  tz6.12f  6375  dfac12lem2  9179  wunex2  9773  ltordlem  10766  prodfdiv  14848  iscatd2  16564  yoniso  17147  mrcmndind  17588  gsum2dlem2  18591  isdrngrd  18996  frlmphl  20343  frlmup1  20360  mdetralt  20637  mdetunilem9  20649  neiptoptop  21158  neiptopnei  21159  cnextcn  22093  cnextfres1  22094  ustuqtop4  22270  dscmet  22599  nrmmetd  22601  rolle  23973  numclwlk2lem2f1o  27562  numclwlk2lem2f1oOLD  27569  chscllem2  28828  esumcvg  30479  eulerpartlemgvv  30769  eulerpartlemn  30774  bnj1326  31423  fwddifnp1  32600  poimirlem13  33754  poimirlem14  33755  poimirlem25  33766  poimirlem31  33772  ftc1anclem7  33823  ftc1anc  33825  fdc  33873  fdc1  33874  iscringd  34129  ismrcd2  37783  fphpdo  37902  monotoddzzfi  38028  monotoddzz  38029  mendlmod  38284  dvgrat  39032  cvgdvgrat  39033  binomcxplemnotnn0  39076  iunincfi  39790  wessf1ornlem  39889  monoords  40029  limcperiod  40382  sumnnodd  40384  cncfshift  40609  cncfperiod  40614  icccncfext  40622  fperdvper  40655  dvnprodlem1  40683  dvnprodlem2  40684  dvnprodlem3  40685  iblspltprt  40711  itgspltprt  40717  stoweidlem43  40782  stoweidlem62  40801  dirkercncflem2  40843  fourierdlem12  40858  fourierdlem15  40861  fourierdlem34  40880  fourierdlem41  40887  fourierdlem42  40888  fourierdlem48  40893  fourierdlem50  40895  fourierdlem51  40896  fourierdlem73  40918  fourierdlem79  40924  fourierdlem81  40926  fourierdlem83  40928  fourierdlem92  40937  fourierdlem94  40939  fourierdlem103  40948  fourierdlem104  40949  fourierdlem111  40956  fourierdlem112  40957  fourierdlem113  40958  etransclem2  40975  etransclem46  41019  intsaluni  41069  meaiuninclem  41219  meaiuninc3v  41223  meaiininclem  41225  ovn0lem  41304  hoidmvlelem2  41335  hoidmvlelem3  41336  hspmbllem2  41366  vonioo  41421  vonicc  41424  pimincfltioc  41451  smflimlem4  41507
  Copyright terms: Public domain W3C validator