MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeqan12d Unicode version

Theorem eqeqan12d 2480
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Hypotheses
Ref Expression
eqeqan12d.1
eqeqan12d.2
Assertion
Ref Expression
eqeqan12d

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . . 3
21adantr 465 . 2
3 eqeqan12d.2 . . 3
43adantl 466 . 2
52, 4eqeq12d 2479 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395
This theorem is referenced by:  eqeqan12rd  2482  eqfnfv2  5982  f1mpt  6169  soisores  6223  xpopth  6839  f1o2ndf1  6908  fnwelem  6915  fnse  6917  tz7.48lem  7125  ecopoveq  7431  xpdom2  7632  unfilem2  7805  wemaplem1  7992  suc11reg  8057  oemapval  8123  cantnf  8133  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  r0weon  8411  infxpen  8413  fodomacn  8458  sornom  8678  fin1a2lem2  8802  fin1a2lem4  8804  neg11  9893  subeqrev  10007  rpnnen1  11242  cnref1o  11244  xneg11  11443  injresinj  11926  modadd1  12033  modmul1  12040  sq11  12240  hashen  12420  fz1eqb  12426  eqwrd  12582  s111  12623  wrd2ind  12703  wwlktovf1  12895  cj11  12995  sqrt11  13096  sqabs  13140  recan  13169  reeff1  13855  efieq  13898  xpnnenOLD  13943  eulerthlem2  14312  vdwlem12  14510  xpsff1o  14965  ismhm  15968  gsmsymgreq  16457  symgfixf1  16462  odf1  16584  sylow1  16623  frgpuplem  16790  isdomn  17943  cygznlem3  18608  psgnghm  18616  tgtop11  19484  fclsval  20509  vitali  22022  recosf1o  22922  dvdsmulf1o  23470  fsumvma  23488  brcgr  24203  axlowdimlem15  24259  axcontlem1  24267  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  iswlk  24520  istrl  24539  wlknwwlkninj  24711  wlkiswwlkinj  24718  wwlkextinj  24730  clwwlkf1  24796  numclwlk1lem2f1  25094  grpoinvf  25242  hial2eq2  26024  erdszelem9  28643  mrsubff1  28874  msubff1  28916  mvhf1  28919  nodenselem5  29445  fneval  30170  topfneec2  30174  ismtyval  30296  wepwsolem  30987  fnwe2val  30995  aomclem8  31007  ismgmhm  32471  2zlidl  32740  bnj554  33957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449
  Copyright terms: Public domain W3C validator