Theorem eqeq12i 2836

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

Syntax hints:   ↔ wb 208   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  neeq12i  3082  rabbi  3383  unineq  4254  sbceqg  4361  sbceqi  4362  preq2b  4778  preqr2  4780  otth  5376  otthg  5377  rncoeq  5846  fresaunres1  6551  eqfnov  7280  mpo2eqb  7283  f1o2ndf1  7818  wfrlem5  7959  ecopovsym  8399  karden  9324  adderpqlem  10376  mulerpqlem  10377  addcmpblnr  10491  ax1ne0  10582  addid1  10820  sq11i  13555  nn0opth2i  13632  oppgcntz  18492  islpir  20022  evlsval  20299  volfiniun  24148  dvmptfsum  24572  axlowdimlem13  26740  usgredg2v  27009  issubgr  27053  clwlkcompbp  27563  pjneli  29500  madjusmdetlem1  31092  breprexp  31904  bnj553  32170  bnj1253  32289  gonanegoal  32599  goalrlem  32643  goalr  32644  fmlasucdisj  32646  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  fprlem1  33137  frrlem15  33142  sltval2  33163  sltsolem1  33180  nosepnelem  33184  nolt02o  33199  altopthsn  33422  bj-2upleq  34327  relowlpssretop  34648  iscrngo2  35290  extid  35583  cdleme18d  37446  fphpd  39433  rp-fakeuninass  39902  relexp0eq  40066  comptiunov2i  40071  clsk1indlem1  40415  ntrclskb  40439  onfrALTlem5  40896  onfrALTlem4  40897  onfrALTlem5VD  41239  onfrALTlem4VD  41240  dvnprodlem3  42253  sge0xadd  42737  reuabaiotaiota  43307  rrx2linest  44749