Theorem eqeq12i 2749

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

Syntax hints:   ↔ wb 205   = wceq 1541

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  neeq12i  3006  rabbi  3430  unineq  4242  vn0  4303  sbceqg  4374  sbceqi  4375  preq2b  4810  preqr2  4812  otth  5446  otthg  5447  rncoeq  5935  fresaunres1  6720  eqfnov  7490  mpo2eqb  7493  f1o2ndf1  8059  fprlem1  8236  wfrlem5OLD  8264  ecopovsym  8765  frrlem15  9702  karden  9840  adderpqlem  10899  mulerpqlem  10900  addcmpblnr  11014  ax1ne0  11105  addrid  11344  sq11i  14105  nn0opth2i  14181  oppgcntz  19159  islpir  20778  evlsval  21533  volfiniun  24948  dvmptfsum  25376  sltval2  27041  sltsolem1  27060  nosepnelem  27064  nolt02o  27080  axlowdimlem13  27966  usgredg2v  28238  issubgr  28282  clwlkcompbp  28793  pjneli  30728  indifbi  31511  madjusmdetlem1  32497  breprexp  33335  bnj553  33599  bnj1253  33718  gonanegoal  34033  goalrlem  34077  goalr  34078  fmlasucdisj  34080  satffunlem  34082  satffunlem1lem1  34083  satffunlem2lem1  34085  altopthsn  34622  bj-2upleq  35556  relowlpssretop  35908  iscrngo2  36529  extid  36844  cdleme18d  38831  fphpd  41197  oenassex  41711  rp-fakeuninass  41910  relexp0eq  42095  comptiunov2i  42100  clsk1indlem1  42439  ntrclskb  42463  onfrALTlem5  42946  onfrALTlem4  42947  onfrALTlem5VD  43289  onfrALTlem4VD  43290  dvnprodlem3  44309  sge0xadd  44796  reuabaiotaiota  45439  rrx2linest  46948