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

Theorem chvarv 2299
 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 2059. (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 2296 . 2 (∀𝑥𝜑𝜓)
3 chvarv.2 . 2 𝜑
42, 3mpg 1764 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 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745 This theorem is referenced by:  axext3ALT  2634  axrep1  4805  axsep2  4815  isso2i  5096  tz6.12f  6250  dfac12lem2  9004  wunex2  9598  ltordlem  10591  prodfdiv  14672  iscatd2  16389  yoniso  16972  mrcmndind  17413  gsum2dlem2  18416  isdrngrd  18821  frlmphl  20168  frlmup1  20185  mdetralt  20462  mdetunilem9  20474  neiptoptop  20983  neiptopnei  20984  cnextcn  21918  cnextfres1  21919  ustuqtop4  22095  dscmet  22424  nrmmetd  22426  rolle  23798  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  chscllem2  28625  esumcvg  30276  eulerpartlemgvv  30566  eulerpartlemn  30571  bnj1326  31220  fwddifnp1  32397  poimirlem13  33552  poimirlem14  33553  poimirlem25  33564  poimirlem31  33570  ftc1anclem7  33621  ftc1anc  33623  fdc  33671  fdc1  33672  iscringd  33927  ismrcd2  37579  fphpdo  37698  monotoddzzfi  37824  monotoddzz  37825  mendlmod  38080  dvgrat  38828  cvgdvgrat  38829  binomcxplemnotnn0  38872  iunincfi  39586  wessf1ornlem  39685  monoords  39825  limcperiod  40178  sumnnodd  40180  cncfshift  40405  cncfperiod  40410  icccncfext  40418  fperdvper  40451  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  iblspltprt  40507  itgspltprt  40513  stoweidlem43  40578  stoweidlem62  40597  dirkercncflem2  40639  fourierdlem12  40654  fourierdlem15  40657  fourierdlem34  40676  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem50  40691  fourierdlem51  40692  fourierdlem73  40714  fourierdlem79  40720  fourierdlem81  40722  fourierdlem83  40724  fourierdlem92  40733  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  etransclem2  40771  etransclem46  40815  intsaluni  40865  meaiuninclem  41015  meaiuninc3v  41019  meaiininclem  41021  ovn0lem  41100  hoidmvlelem2  41131  hoidmvlelem3  41132  hspmbllem2  41162  vonioo  41217  vonicc  41220  pimincfltioc  41247  smflimlem4  41303
 Copyright terms: Public domain W3C validator