Theorem eqeq12i 2665

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

Syntax hints:   ↔ wb 196   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  neeq12i  2889  rabbi  3150  unineq  3910  sbceqg  4017  rabeqsn  4246  preq2b  4410  preqr2  4412  iuneq12df  4576  otth  4982  otthg  4983  rncoeq  5421  fresaunres1  6115  eqfnov  6808  mpt22eqb  6811  f1o2ndf1  7330  wfrlem5  7464  ecopovsym  7892  karden  8796  adderpqlem  9814  mulerpqlem  9815  addcmpblnr  9928  ax1ne0  10019  addid1  10254  sq11i  12994  nn0opth2i  13098  oppgcntz  17840  islpir  19297  evlsval  19567  volfiniun  23361  dvmptfsum  23783  axlowdimlem13  25879  usgredg2v  26164  issubgr  26208  pjneli  28710  iuneq12daf  29499  madjusmdetlem1  30021  breprexp  30839  bnj553  31094  bnj1253  31211  frrlem5  31909  sltval2  31934  sltsolem1  31951  nosepnelem  31955  nolt02o  31970  altopthsn  32193  bj-2upleq  33125  relowlpssretop  33342  iscrngo2  33926  sbceqi  34043  extid  34222  cdleme18d  35900  fphpd  37697  rp-fakeuninass  38179  relexp0eq  38310  comptiunov2i  38315  clsk1indlem1  38660  ntrclskb  38684  onfrALTlem5  39074  onfrALTlem4  39075  onfrALTlem5VD  39435  onfrALTlem4VD  39436  dvnprodlem3  40481  sge0xadd  40970