Theorem eqeq12i 2487

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	|- A = B
eqeq12i.2	|- C = D

Assertion

Ref	Expression
eqeq12i	|- ( A = C <-> B = D )

Proof of Theorem eqeq12i

Step	Hyp	Ref	Expression
1		eqeq12i.1	. . 3 |- A = B
2	1	eqeq1i 2474	. 2 |- ( A = C <-> B = C )
3		eqeq12i.2	. . 3 |- C = D
4	3	eqeq2i 2485	. 2 |- ( B = C <-> B = D )
5	2, 4	bitri 249	1 |- ( A = C <-> B = D )

Syntax hints:   <-> wb 184   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  neeq12i  2756  rabbi  3045  csbeq2  3444  unineq  3753  sbceqg  3830  preqr2  4207  iuneq12df  4355  otth  4735  otthg  4736  rncoeq  5272  fresaunres1  5764  eqfnov  6403  mpt22eqb  6406  f1o2ndf1  6903  ecopovsym  7425  karden  8325  adderpqlem  9344  mulerpqlem  9345  addcmpblnr  9458  ax1ne0  9549  addid1  9771  sq11i  12238  nn0opth2i  12331  oppgcntz  16271  islpir  17767  evlsval  18058  volfiniun  21825  dvmptfsum  22244  axlowdimlem13  24071  usgraidx2v  24207  el2wlkonotot0  24686  pjneli  26455  iuneq12daf  27239  sspred  29170  wfrlem5  29265  frrlem5  29309  sltval2  29334  sltsolem1  29346  altopthsn  29529  iscrngo2  30313  sbceqi  30431  fphpd  30669  usgedgvadf1  32196  usgedgvadf1ALT  32199  rabeqsn  32353  onfrALTlem5  32750  onfrALTlem4  32751  onfrALTlem5VD  33121  onfrALTlem4VD  33122  bnj553  33391  bnj1253  33508  bj-2upleq  34007  cdleme18d  35447