Theorem eqeq12i 2442

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

Syntax hints:   <-> wb 187   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-cleq 2414

This theorem is referenced by:  neeq12i  2709  rabbi  3004  unineq  3723  sbceqg  3803  preqr2  4175  iuneq12df  4323  otth  4703  otthg  4704  rncoeq  5117  sspred  5407  fresaunres1  5773  eqfnov  6416  mpt22eqb  6419  f1o2ndf1  6915  wfrlem5  7051  ecopovsym  7476  karden  8374  adderpqlem  9386  mulerpqlem  9387  addcmpblnr  9500  ax1ne0  9591  addid1  9820  sq11i  12371  nn0opth2i  12463  oppgcntz  17014  islpir  18472  evlsval  18741  volfiniun  22498  dvmptfsum  22925  axlowdimlem13  24982  usgraidx2v  25118  el2wlkonotot0  25598  pjneli  27374  iuneq12daf  28172  madjusmdetlem1  28661  bnj553  29717  bnj1253  29834  frrlem5  30525  sltval2  30550  sltsolem1  30562  altopthsn  30733  bj-2upleq  31574  relowlpssretop  31731  iscrngo2  32195  sbceqi  32312  cdleme18d  33830  fphpd  35628  rp-fakeuninass  36131  relexp0eq  36263  comptiunov2i  36268  onfrALTlem5  36878  onfrALTlem4  36879  onfrALTlem5VD  37255  onfrALTlem4VD  37256  dvnprodlem3  37763  sge0xadd  38185  usgridx2v  39087  issubgr  39116  usgedgvadf1  39346  usgedgvadf1ALT  39349  rabeqsn  39732