Theorem eqeq12i 2757

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

Syntax hints:   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  neeq12i  3000  rabbi  3421  unineq  4216  vn0  4273  sbceqg  4340  sbceqi  4341  preq2b  4778  preqr2  4780  otth  5424  otthg  5425  rncoeq  5924  fresaunres1  6700  eqfnov  7485  mpo2eqb  7488  f1o2ndf1  8061  fprlem1  8240  ecopovsym  8756  frrlem15  9672  karden  9810  adderpqlem  10868  mulerpqlem  10869  addcmpblnr  10983  ax1ne0  11074  addrid  11317  sq11i  14144  nn0opth2i  14224  oppgcntz  19330  opprdomnb  20689  isdomn4r  20691  islpir  21321  evlsval  22062  volfiniun  25532  dvmptfsum  25960  ltsval2  27638  ltssolem1  27657  nosepnelem  27661  nolt02o  27677  axlowdimlem13  29041  usgredg2v  29314  issubgr  29358  clwlkcompbp  29868  pjneli  31812  indifbi  32608  madjusmdetlem1  34011  breprexp  34817  bnj553  35080  bnj1253  35199  gonanegoal  35580  goalrlem  35624  goalr  35625  fmlasucdisj  35627  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  altopthsn  36189  bj-2upleq  37365  relowlpssretop  37726  iscrngo2  38364  extid  38683  cdleme18d  40787  fphpd  43261  oenassex  43763  rp-fakeuninass  43960  relexp0eq  44145  comptiunov2i  44150  clsk1indlem1  44489  ntrclskb  44513  onfrALTlem5  44986  onfrALTlem4  44987  onfrALTlem5VD  45328  onfrALTlem4VD  45329  dvnprodlem3  46391  sge0xadd  46878  reuabaiotaiota  47550  rrx2linest  49233  fucofvalne  49815