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

Theorem chvarv 2261
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 2017. (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 2258 . 2 (∀𝑥𝜑𝜓)
3 chvarv.2 . 2 𝜑
42, 3mpg 1722 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 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045  ax-13 2244
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  axext3ALT  2603  axrep1  4763  axsep2  4773  isso2i  5057  tz6.12f  6199  dfac12lem2  8951  wunex2  9545  ltordlem  10538  prodfdiv  14609  iscatd2  16323  yoniso  16906  mrcmndind  17347  gsum2dlem2  18351  isdrngrd  18754  frlmphl  20101  frlmup1  20118  mdetralt  20395  mdetunilem9  20407  neiptoptop  20916  neiptopnei  20917  cnextcn  21852  cnextfres1  21853  ustuqtop4  22029  dscmet  22358  nrmmetd  22360  rolle  23734  numclwlk2lem2f1o  27209  chscllem2  28467  esumcvg  30122  eulerpartlemgvv  30412  eulerpartlemn  30417  bnj1326  31068  fwddifnp1  32247  poimirlem13  33393  poimirlem14  33394  poimirlem25  33405  poimirlem31  33411  ftc1anclem7  33462  ftc1anc  33464  fdc  33512  fdc1  33513  iscringd  33768  ismrcd2  37081  fphpdo  37200  monotoddzzfi  37326  monotoddzz  37327  mendlmod  37582  dvgrat  38331  cvgdvgrat  38332  binomcxplemnotnn0  38375  iunincfi  39092  wessf1ornlem  39187  monoords  39324  limcperiod  39660  sumnnodd  39662  cncfshift  39850  cncfperiod  39855  icccncfext  39863  fperdvper  39896  dvnprodlem1  39924  dvnprodlem2  39925  dvnprodlem3  39926  iblspltprt  39952  itgspltprt  39958  stoweidlem43  40023  stoweidlem62  40042  dirkercncflem2  40084  fourierdlem12  40099  fourierdlem15  40102  fourierdlem34  40121  fourierdlem41  40128  fourierdlem42  40129  fourierdlem48  40134  fourierdlem50  40136  fourierdlem51  40137  fourierdlem73  40159  fourierdlem79  40165  fourierdlem81  40167  fourierdlem83  40169  fourierdlem92  40178  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem111  40197  fourierdlem112  40198  fourierdlem113  40199  etransclem2  40216  etransclem46  40260  intsaluni  40310  meaiuninclem  40460  meaiininclem  40463  ovn0lem  40542  hoidmvlelem2  40573  hoidmvlelem3  40574  hspmbllem2  40604  vonioo  40659  vonicc  40662  pimincfltioc  40689  smflimlem4  40745
  Copyright terms: Public domain W3C validator