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 275	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)

Syntax hints:   ↔ wb 206   = wceq 1541

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  neeq12i  2994  rabbi  3425  unineq  4235  vn0  4292  sbceqg  4359  sbceqi  4360  preq2b  4796  preqr2  4798  otth  5422  otthg  5423  rncoeq  5920  fresaunres1  6696  eqfnov  7475  mpo2eqb  7478  f1o2ndf1  8052  fprlem1  8230  ecopovsym  8743  frrlem15  9650  karden  9788  adderpqlem  10845  mulerpqlem  10846  addcmpblnr  10960  ax1ne0  11051  addrid  11293  sq11i  14098  nn0opth2i  14178  oppgcntz  19276  opprdomnb  20632  isdomn4r  20634  islpir  21265  evlsval  22021  volfiniun  25475  dvmptfsum  25906  sltval2  27595  sltsolem1  27614  nosepnelem  27618  nolt02o  27634  axlowdimlem13  28932  usgredg2v  29205  issubgr  29249  clwlkcompbp  29760  pjneli  31703  indifbi  32500  madjusmdetlem1  33840  breprexp  34646  bnj553  34910  bnj1253  35029  gonanegoal  35396  goalrlem  35440  goalr  35441  fmlasucdisj  35443  satffunlem  35445  satffunlem1lem1  35446  satffunlem2lem1  35448  altopthsn  36003  bj-2upleq  37054  relowlpssretop  37406  iscrngo2  38045  extid  38352  cdleme18d  40342  fphpd  42857  oenassex  43359  rp-fakeuninass  43557  relexp0eq  43742  comptiunov2i  43747  clsk1indlem1  44086  ntrclskb  44110  onfrALTlem5  44583  onfrALTlem4  44584  onfrALTlem5VD  44925  onfrALTlem4VD  44926  dvnprodlem3  45994  sge0xadd  46481  reuabaiotaiota  47126  rrx2linest  48782  fucofvalne  49365