Theorem eqeq12i 2752

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

Syntax hints:   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  neeq12i  2996  rabbi  3427  unineq  4238  vn0  4295  sbceqg  4362  sbceqi  4363  preq2b  4801  preqr2  4803  otth  5430  otthg  5431  rncoeq  5929  fresaunres1  6705  eqfnov  7485  mpo2eqb  7488  f1o2ndf1  8062  fprlem1  8240  ecopovsym  8754  frrlem15  9667  karden  9805  adderpqlem  10863  mulerpqlem  10864  addcmpblnr  10978  ax1ne0  11069  addrid  11311  sq11i  14112  nn0opth2i  14192  oppgcntz  19291  opprdomnb  20648  isdomn4r  20650  islpir  21281  evlsval  22039  volfiniun  25502  dvmptfsum  25933  sltval2  27622  sltsolem1  27641  nosepnelem  27645  nolt02o  27661  axlowdimlem13  28976  usgredg2v  29249  issubgr  29293  clwlkcompbp  29804  pjneli  31747  indifbi  32544  madjusmdetlem1  33933  breprexp  34739  bnj553  35003  bnj1253  35122  gonanegoal  35495  goalrlem  35539  goalr  35540  fmlasucdisj  35542  satffunlem  35544  satffunlem1lem1  35545  satffunlem2lem1  35547  altopthsn  36104  bj-2upleq  37156  relowlpssretop  37508  iscrngo2  38137  extid  38448  cdleme18d  40494  fphpd  43000  oenassex  43502  rp-fakeuninass  43699  relexp0eq  43884  comptiunov2i  43889  clsk1indlem1  44228  ntrclskb  44252  onfrALTlem5  44725  onfrALTlem4  44726  onfrALTlem5VD  45067  onfrALTlem4VD  45068  dvnprodlem3  46134  sge0xadd  46621  reuabaiotaiota  47275  rrx2linest  48930  fucofvalne  49512