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

Theorem chvarv 2251
 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 2006. (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 2248 . 2 (∀𝑥𝜑𝜓)
3 chvarv.2 . 2 𝜑
42, 3mpg 1715 1 𝜓
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696 This theorem is referenced by:  axext3ALT  2593  axrep1  4700  axsep2  4710  isso2i  4991  tz6.12f  6122  dfac12lem2  8849  wunex2  9439  ltordlem  10432  prodfdiv  14467  iscatd2  16165  yoniso  16748  mrcmndind  17189  gsum2dlem2  18193  isdrngrd  18596  frlmphl  19939  frlmup1  19956  mdetralt  20233  mdetunilem9  20245  neiptoptop  20745  neiptopnei  20746  cnextcn  21681  cnextfres1  21682  ustuqtop4  21858  dscmet  22187  nrmmetd  22189  rolle  23557  numclwlk2lem2f1o  26632  chscllem2  27881  esumcvg  29475  eulerpartlemgvv  29765  eulerpartlemn  29770  bnj1326  30348  fwddifnp1  31442  poimirlem13  32592  poimirlem14  32593  poimirlem25  32604  poimirlem31  32610  ftc1anclem7  32661  ftc1anc  32663  fdc  32711  fdc1  32712  iscringd  32967  ismrcd2  36280  fphpdo  36399  monotoddzzfi  36525  monotoddzz  36526  mendlmod  36782  dvgrat  37533  cvgdvgrat  37534  binomcxplemnotnn0  37577  iunincfi  38300  wessf1ornlem  38366  monoords  38452  limcperiod  38695  sumnnodd  38697  cncfshift  38759  cncfperiod  38764  icccncfext  38773  fperdvper  38808  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  iblspltprt  38865  itgspltprt  38871  stoweidlem43  38936  stoweidlem62  38955  dirkercncflem2  38997  fourierdlem12  39012  fourierdlem15  39015  fourierdlem34  39034  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem50  39049  fourierdlem51  39050  fourierdlem73  39072  fourierdlem79  39078  fourierdlem81  39080  fourierdlem83  39082  fourierdlem92  39091  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  etransclem2  39129  etransclem46  39173  intsaluni  39223  meaiuninclem  39373  meaiininclem  39376  ovn0lem  39455  hoidmvlelem2  39486  hoidmvlelem3  39487  hspmbllem2  39517  vonioo  39573  vonicc  39576  pimincfltioc  39603  smflimlem4  39660  av-numclwlk2lem2f1o  41535
 Copyright terms: Public domain W3C validator