Theorem eqeq12i 2753

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

Syntax hints:   ↔ wb 206   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  neeq12i  3005  rabbi  3465  unineq  4294  vn0  4351  sbceqg  4418  sbceqi  4419  preq2b  4852  preqr2  4854  otth  5495  otthg  5496  rncoeq  5993  fresaunres1  6782  eqfnov  7562  mpo2eqb  7565  f1o2ndf1  8146  fprlem1  8324  wfrlem5OLD  8352  ecopovsym  8858  frrlem15  9795  karden  9933  adderpqlem  10992  mulerpqlem  10993  addcmpblnr  11107  ax1ne0  11198  addrid  11439  sq11i  14227  nn0opth2i  14307  oppgcntz  19398  opprdomnb  20734  isdomn4r  20736  islpir  21356  evlsval  22128  volfiniun  25596  dvmptfsum  26028  sltval2  27716  sltsolem1  27735  nosepnelem  27739  nolt02o  27755  axlowdimlem13  28984  usgredg2v  29259  issubgr  29303  clwlkcompbp  29815  pjneli  31752  indifbi  32548  madjusmdetlem1  33788  breprexp  34627  bnj553  34891  bnj1253  35010  gonanegoal  35337  goalrlem  35381  goalr  35382  fmlasucdisj  35384  satffunlem  35386  satffunlem1lem1  35387  satffunlem2lem1  35389  altopthsn  35943  bj-2upleq  36995  relowlpssretop  37347  iscrngo2  37984  extid  38292  cdleme18d  40278  fphpd  42804  oenassex  43308  rp-fakeuninass  43506  relexp0eq  43691  comptiunov2i  43696  clsk1indlem1  44035  ntrclskb  44059  onfrALTlem5  44540  onfrALTlem4  44541  onfrALTlem5VD  44883  onfrALTlem4VD  44884  dvnprodlem3  45904  sge0xadd  46391  reuabaiotaiota  47037  rrx2linest  48592