Theorem eqeq12i 2785

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

Syntax hints:   ↔ wb 196   = wceq 1631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764

This theorem is referenced by:  neeq12i  3009  rabbi  3269  unineq  4026  sbceqg  4129  rabeqsn  4353  preq2b  4511  preqr2  4513  iuneq12df  4679  otth  5081  otthg  5082  rncoeq  5526  fresaunres1  6218  eqfnov  6917  mpt22eqb  6920  f1o2ndf1  7440  wfrlem5  7576  ecopovsym  8006  karden  8926  adderpqlem  9982  mulerpqlem  9983  addcmpblnr  10096  ax1ne0  10187  addid1  10422  sq11i  13161  nn0opth2i  13262  oppgcntz  18001  islpir  19464  evlsval  19734  volfiniun  23535  dvmptfsum  23958  axlowdimlem13  26055  usgredg2v  26341  issubgr  26386  clwlkcompbp  26913  pjneli  28922  iuneq12daf  29711  madjusmdetlem1  30233  breprexp  31051  bnj553  31306  bnj1253  31423  frrlem5  32121  sltval2  32146  sltsolem1  32163  nosepnelem  32167  nolt02o  32182  altopthsn  32405  bj-2upleq  33330  relowlpssretop  33548  iscrngo2  34126  sbceqi  34243  extid  34422  cdleme18d  36103  fphpd  37904  rp-fakeuninass  38386  relexp0eq  38517  comptiunov2i  38522  clsk1indlem1  38867  ntrclskb  38891  onfrALTlem5  39280  onfrALTlem4  39281  onfrALTlem5VD  39641  onfrALTlem4VD  39642  dvnprodlem3  40676  sge0xadd  41164