Theorem eqeq12i 2756

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

Syntax hints:   ↔ wb 205   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  neeq12i  3009  rabbi  3309  unineq  4208  vn0  4269  sbceqg  4340  sbceqi  4341  preq2b  4775  preqr2  4777  otth  5393  otthg  5394  rncoeq  5873  fresaunres1  6631  eqfnov  7381  mpo2eqb  7384  f1o2ndf1  7934  fprlem1  8087  wfrlem5OLD  8115  ecopovsym  8566  frrlem15  9446  karden  9584  adderpqlem  10641  mulerpqlem  10642  addcmpblnr  10756  ax1ne0  10847  addid1  11085  sq11i  13836  nn0opth2i  13913  oppgcntz  18886  islpir  20433  evlsval  21206  volfiniun  24616  dvmptfsum  25044  axlowdimlem13  27225  usgredg2v  27497  issubgr  27541  clwlkcompbp  28051  pjneli  29986  indifbi  30769  madjusmdetlem1  31679  breprexp  32513  bnj553  32778  bnj1253  32897  gonanegoal  33214  goalrlem  33258  goalr  33259  fmlasucdisj  33261  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  sltval2  33786  sltsolem1  33805  nosepnelem  33809  nolt02o  33825  altopthsn  34190  bj-2upleq  35129  relowlpssretop  35462  iscrngo2  36082  extid  36373  cdleme18d  38236  fphpd  40554  rp-fakeuninass  41021  relexp0eq  41198  comptiunov2i  41203  clsk1indlem1  41544  ntrclskb  41568  onfrALTlem5  42051  onfrALTlem4  42052  onfrALTlem5VD  42394  onfrALTlem4VD  42395  dvnprodlem3  43379  sge0xadd  43863  reuabaiotaiota  44466  rrx2linest  45976