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

Theorem eqeq12i 2477
 Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Hypotheses
Ref Expression
eqeq12i.1
eqeq12i.2
Assertion
Ref Expression
eqeq12i

Proof of Theorem eqeq12i
StepHypRef Expression
1 eqeq12i.1 . . 3
21eqeq1i 2464 . 2
3 eqeq12i.2 . . 3
43eqeq2i 2475 . 2
52, 4bitri 249 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395 This theorem is referenced by:  neeq12i  2746  rabbi  3036  unineq  3747  sbceqg  3825  preqr2  4205  iuneq12df  4354  otth  4734  otthg  4735  rncoeq  5271  fresaunres1  5763  eqfnov  6408  mpt22eqb  6411  f1o2ndf1  6908  ecopovsym  7432  karden  8334  adderpqlem  9353  mulerpqlem  9354  addcmpblnr  9467  ax1ne0  9558  addid1  9781  sq11i  12258  nn0opth2i  12351  oppgcntz  16399  islpir  17897  evlsval  18188  volfiniun  21957  dvmptfsum  22376  axlowdimlem13  24257  usgraidx2v  24393  el2wlkonotot0  24872  pjneli  26641  iuneq12daf  27425  sspred  29252  wfrlem5  29347  frrlem5  29391  sltval2  29416  sltsolem1  29428  altopthsn  29611  iscrngo2  30395  sbceqi  30513  fphpd  30750  dvnprodlem3  31745  usgedgvadf1  32415  usgedgvadf1ALT  32418  rabeqsn  32919  onfrALTlem5  33314  onfrALTlem4  33315  onfrALTlem5VD  33685  onfrALTlem4VD  33686  bnj553  33956  bnj1253  34073  bj-2upleq  34570  cdleme18d  36020  rp-fakeuninass  37741 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-cleq 2449
 Copyright terms: Public domain W3C validator