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

Step	Hyp	Ref	Expression
1		eqeq12i.1	. . 3
2	1	eqeq1i 2464	. 2
3		eqeq12i.2	. . 3
4	3	eqeq2i 2475	. 2
5	2, 4	bitri 249	1

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