Theorem eqeq12i 2636

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

Syntax hints:   ↔ wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  neeq12i  2860  rabbi  3120  unineq  3877  sbceqg  3984  rabeqsn  4214  preq2b  4378  preqr2  4381  iuneq12df  4544  otth  4953  otthg  4954  rncoeq  5389  fresaunres1  6077  eqfnov  6766  mpt22eqb  6769  f1o2ndf1  7285  wfrlem5  7419  ecopovsym  7849  karden  8758  adderpqlem  9776  mulerpqlem  9777  addcmpblnr  9890  ax1ne0  9981  addid1  10216  sq11i  12954  nn0opth2i  13058  oppgcntz  17794  islpir  19249  evlsval  19519  volfiniun  23315  dvmptfsum  23738  axlowdimlem13  25834  usgredg2v  26119  issubgr  26163  pjneli  28582  iuneq12daf  29373  madjusmdetlem1  29893  breprexp  30711  bnj553  30968  bnj1253  31085  frrlem5  31784  sltval2  31809  sltsolem1  31826  nosepnelem  31830  nolt02o  31845  altopthsn  32068  bj-2upleq  33000  relowlpssretop  33212  iscrngo2  33796  sbceqi  33913  extid  34081  cdleme18d  35582  fphpd  37380  rp-fakeuninass  37862  relexp0eq  37993  comptiunov2i  37998  clsk1indlem1  38343  ntrclskb  38367  onfrALTlem5  38757  onfrALTlem4  38758  onfrALTlem5VD  39121  onfrALTlem4VD  39122  dvnprodlem3  40163  sge0xadd  40652