Theorem eqeq12i 2820

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

Syntax hints:   ↔ wb 197   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799

This theorem is referenced by:  neeq12i  3044  rabbi  3309  unineq  4079  sbceqg  4181  preq2b  4566  preqr2  4568  iuneq12df  4736  otth  5142  otthg  5143  rncoeq  5590  fresaunres1  6288  eqfnov  6992  mpt22eqb  6995  f1o2ndf1  7515  wfrlem5  7651  ecopovsym  8081  karden  9001  adderpqlem  10057  mulerpqlem  10058  addcmpblnr  10171  ax1ne0  10262  addid1  10497  sq11i  13173  nn0opth2i  13274  oppgcntz  17991  islpir  19454  evlsval  19723  volfiniun  23527  dvmptfsum  23951  axlowdimlem13  26047  usgredg2v  26333  issubgr  26378  clwlkcompbp  26905  pjneli  28909  iuneq12daf  29697  madjusmdetlem1  30217  breprexp  31035  bnj553  31289  bnj1253  31406  frrlem5  32103  sltval2  32128  sltsolem1  32145  nosepnelem  32149  nolt02o  32164  altopthsn  32387  bj-2upleq  33308  relowlpssretop  33526  iscrngo2  34105  sbceqi  34222  extid  34395  cdleme18d  36073  fphpd  37879  rp-fakeuninass  38359  relexp0eq  38490  comptiunov2i  38495  clsk1indlem1  38840  ntrclskb  38864  onfrALTlem5  39252  onfrALTlem4  39253  onfrALTlem5VD  39612  onfrALTlem4VD  39613  dvnprodlem3  40640  sge0xadd  41128  reuabaiotaiota  41668