Theorem eqeq12i 2474

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 2461	. 2 |- ( A = C <-> B = C )
3		eqeq12i.2	. . 3 |- C = D
4	3	eqeq2i 2472	. 2 |- ( B = C <-> B = D )
5	2, 4	bitri 249	1 |- ( A = C <-> B = D )

Syntax hints:   <-> wb 184   = wceq 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

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

This theorem is referenced by:  neeq12i  2741  rabbi  3005  csbeq2  3402  unineq  3711  sbceqg  3788  preqr2  4158  iuneq12df  4305  otth  4685  rncoeq  5214  fresaunres1  5695  eqfnov  6309  mpt22eqb  6312  f1o2ndf1  6793  ecopovsym  7315  karden  8216  adderpqlem  9237  mulerpqlem  9238  addcmpblnr  9353  ax1ne0  9441  addid1  9663  sq11i  12076  nn0opth2i  12169  oppgcntz  16001  islpir  17457  evlsval  17732  volfiniun  21164  dvmptfsum  21583  axlowdimlem13  23372  usgraidx2v  23483  pjneli  25298  iuneq12daf  26079  gsumvsca1  26416  gsumvsca2  26417  sspred  27797  wfrlem5  27892  frrlem5  27936  sltval2  27961  sltsolem1  27973  altopthsn  28156  iscrngo2  28966  sbceqi  29084  fphpd  29323  otthg  30298  el2wlkonotot0  30559  rabeqsn  30885  onfrALTlem5  31602  onfrALTlem4  31603  onfrALTlem5VD  31973  onfrALTlem4VD  31974  bnj553  32243  bnj1253  32360  bj-2upleq  32857  cdleme18d  34297