Theorem eqeq12i 2747

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  neeq12i  2991  rabbi  3433  unineq  4247  vn0  4304  sbceqg  4371  sbceqi  4372  preq2b  4807  preqr2  4809  otth  5439  otthg  5440  rncoeq  5932  fresaunres1  6715  eqfnov  7498  mpo2eqb  7501  f1o2ndf1  8078  fprlem1  8256  ecopovsym  8769  frrlem15  9686  karden  9824  adderpqlem  10883  mulerpqlem  10884  addcmpblnr  10998  ax1ne0  11089  addrid  11330  sq11i  14132  nn0opth2i  14212  oppgcntz  19278  opprdomnb  20637  isdomn4r  20639  islpir  21270  evlsval  22026  volfiniun  25481  dvmptfsum  25912  sltval2  27601  sltsolem1  27620  nosepnelem  27624  nolt02o  27640  axlowdimlem13  28934  usgredg2v  29207  issubgr  29251  clwlkcompbp  29762  pjneli  31702  indifbi  32499  madjusmdetlem1  33810  breprexp  34617  bnj553  34881  bnj1253  35000  gonanegoal  35332  goalrlem  35376  goalr  35377  fmlasucdisj  35379  satffunlem  35381  satffunlem1lem1  35382  satffunlem2lem1  35384  altopthsn  35942  bj-2upleq  36993  relowlpssretop  37345  iscrngo2  37984  extid  38291  cdleme18d  40282  fphpd  42797  oenassex  43300  rp-fakeuninass  43498  relexp0eq  43683  comptiunov2i  43688  clsk1indlem1  44027  ntrclskb  44051  onfrALTlem5  44525  onfrALTlem4  44526  onfrALTlem5VD  44867  onfrALTlem4VD  44868  dvnprodlem3  45939  sge0xadd  46426  reuabaiotaiota  47081  rrx2linest  48724  fucofvalne  49307