Theorem eqeq12i 2756

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 2743	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3		eqeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	eqeq2i 2751	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)
5	2, 4	bitri 274	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)

Syntax hints:   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  neeq12i  3010  rabbi  3316  unineq  4211  vn0  4272  sbceqg  4343  sbceqi  4344  preq2b  4778  preqr2  4780  otth  5399  otthg  5400  rncoeq  5884  fresaunres1  6647  eqfnov  7403  mpo2eqb  7406  f1o2ndf1  7963  fprlem1  8116  wfrlem5OLD  8144  ecopovsym  8608  frrlem15  9515  karden  9653  adderpqlem  10710  mulerpqlem  10711  addcmpblnr  10825  ax1ne0  10916  addid1  11155  sq11i  13908  nn0opth2i  13985  oppgcntz  18971  islpir  20520  evlsval  21296  volfiniun  24711  dvmptfsum  25139  axlowdimlem13  27322  usgredg2v  27594  issubgr  27638  clwlkcompbp  28150  pjneli  30085  indifbi  30868  madjusmdetlem1  31777  breprexp  32613  bnj553  32878  bnj1253  32997  gonanegoal  33314  goalrlem  33358  goalr  33359  fmlasucdisj  33361  satffunlem  33363  satffunlem1lem1  33364  satffunlem2lem1  33366  sltval2  33859  sltsolem1  33878  nosepnelem  33882  nolt02o  33898  altopthsn  34263  bj-2upleq  35202  relowlpssretop  35535  iscrngo2  36155  extid  36446  cdleme18d  38309  fphpd  40638  rp-fakeuninass  41123  relexp0eq  41309  comptiunov2i  41314  clsk1indlem1  41655  ntrclskb  41679  onfrALTlem5  42162  onfrALTlem4  42163  onfrALTlem5VD  42505  onfrALTlem4VD  42506  dvnprodlem3  43489  sge0xadd  43973  reuabaiotaiota  44579  rrx2linest  46088