Theorem eqeq12i 2751

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

Syntax hints:   ↔ wb 209   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  neeq12i  2998  rabbi  3285  unineq  4178  vn0  4239  sbceqg  4310  sbceqi  4311  preq2b  4744  preqr2  4746  otth  5353  otthg  5354  rncoeq  5829  fresaunres1  6570  eqfnov  7317  mpo2eqb  7320  f1o2ndf1  7869  fprlem1  8019  wfrlem5  8037  ecopovsym  8479  karden  9476  adderpqlem  10533  mulerpqlem  10534  addcmpblnr  10648  ax1ne0  10739  addid1  10977  sq11i  13725  nn0opth2i  13802  oppgcntz  18710  islpir  20241  evlsval  21000  volfiniun  24398  dvmptfsum  24826  axlowdimlem13  26999  usgredg2v  27269  issubgr  27313  clwlkcompbp  27823  pjneli  29758  indifbi  30541  madjusmdetlem1  31445  breprexp  32279  bnj553  32545  bnj1253  32664  gonanegoal  32981  goalrlem  33025  goalr  33026  fmlasucdisj  33028  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  frrlem15  33505  sltval2  33545  sltsolem1  33564  nosepnelem  33568  nolt02o  33584  altopthsn  33949  bj-2upleq  34888  relowlpssretop  35221  iscrngo2  35841  extid  36132  cdleme18d  37995  fphpd  40282  rp-fakeuninass  40749  relexp0eq  40927  comptiunov2i  40932  clsk1indlem1  41273  ntrclskb  41297  onfrALTlem5  41776  onfrALTlem4  41777  onfrALTlem5VD  42119  onfrALTlem4VD  42120  dvnprodlem3  43107  sge0xadd  43591  reuabaiotaiota  44194  rrx2linest  45704