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

Theorem chvarv 2250
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 2005. (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 2247 . 2 (∀𝑥𝜑𝜓)
3 chvarv.2 . 2 𝜑
42, 3mpg 1714 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-13 2233
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  axext3ALT  2592  axrep1  4694  axsep2  4704  isso2i  4980  tz6.12f  6106  dfac12lem2  8826  wunex2  9416  ltordlem  10404  prodfdiv  14415  iscatd2  16113  yoniso  16696  mrcmndind  17137  gsum2dlem2  18141  isdrngrd  18544  frlmphl  19886  frlmup1  19903  mdetralt  20180  mdetunilem9  20192  neiptoptop  20692  neiptopnei  20693  cnextcn  21628  cnextfres1  21629  ustuqtop4  21805  dscmet  22134  nrmmetd  22136  rolle  23501  numclwlk2lem2f1o  26425  chscllem2  27674  esumcvg  29268  eulerpartlemgvv  29558  eulerpartlemn  29563  bnj1326  30141  fwddifnp1  31235  poimirlem13  32375  poimirlem14  32376  poimirlem25  32387  poimirlem31  32393  ftc1anclem7  32444  ftc1anc  32446  fdc  32494  fdc1  32495  iscringd  32750  ismrcd2  36063  fphpdo  36182  monotoddzzfi  36308  monotoddzz  36309  mendlmod  36565  dvgrat  37316  cvgdvgrat  37317  binomcxplemnotnn0  37360  iunincfi  38083  wessf1ornlem  38149  monoords  38235  limcperiod  38478  sumnnodd  38480  cncfshift  38542  cncfperiod  38547  icccncfext  38556  fperdvper  38591  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  iblspltprt  38648  itgspltprt  38654  stoweidlem43  38719  stoweidlem62  38738  dirkercncflem2  38780  fourierdlem12  38795  fourierdlem15  38798  fourierdlem34  38817  fourierdlem41  38824  fourierdlem42  38825  fourierdlem48  38830  fourierdlem50  38832  fourierdlem51  38833  fourierdlem73  38855  fourierdlem79  38861  fourierdlem81  38863  fourierdlem83  38865  fourierdlem92  38874  fourierdlem94  38876  fourierdlem103  38885  fourierdlem104  38886  fourierdlem111  38893  fourierdlem112  38894  fourierdlem113  38895  etransclem2  38912  etransclem46  38956  intsaluni  39006  meaiuninclem  39156  meaiininclem  39159  ovn0lem  39238  hoidmvlelem2  39269  hoidmvlelem3  39270  hspmbllem2  39300  vonioo  39356  vonicc  39359  pimincfltioc  39386  smflimlem4  39443  av-numclwlk2lem2f1o  41516
  Copyright terms: Public domain W3C validator