Theorem eqeq12i 2476

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

Syntax hints:   <-> wb 189   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  neeq12i  2702  rabbi  2981  unineq  3705  sbceqg  3785  rabeqsn  4013  preq2b  4160  preqr2  4163  iuneq12df  4316  otth  4701  otthg  4702  rncoeq  5120  sspred  5411  fresaunres1  5783  eqfnov  6434  mpt22eqb  6437  f1o2ndf1  6936  wfrlem5  7071  ecopovsym  7496  karden  8397  adderpqlem  9410  mulerpqlem  9411  addcmpblnr  9524  ax1ne0  9615  addid1  9844  sq11i  12403  nn0opth2i  12495  oppgcntz  17070  islpir  18528  evlsval  18797  volfiniun  22556  dvmptfsum  22983  axlowdimlem13  25040  usgraidx2v  25176  el2wlkonotot0  25656  pjneli  27432  iuneq12daf  28225  madjusmdetlem1  28704  bnj553  29759  bnj1253  29876  frrlem5  30568  sltval2  30593  sltsolem1  30607  altopthsn  30778  bj-2upleq  31652  relowlpssretop  31813  iscrngo2  32277  sbceqi  32394  cdleme18d  33907  fphpd  35705  rp-fakeuninass  36207  relexp0eq  36339  comptiunov2i  36344  onfrALTlem5  36953  onfrALTlem4  36954  onfrALTlem5VD  37323  onfrALTlem4VD  37324  dvnprodlem3  37909  sge0xadd  38380  usgredg2v  39450  issubgr  39489  usgedgvadf1  40096  usgedgvadf1ALT  40099