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  19272  opprdomnb  20602  isdomn4r  20604  islpir  21214  evlsval  21969  volfiniun  25424  dvmptfsum  25855  sltval2  27544  sltsolem1  27563  nosepnelem  27567  nolt02o  27583  axlowdimlem13  28857  usgredg2v  29130  issubgr  29174  clwlkcompbp  29685  pjneli  31625  indifbi  32422  madjusmdetlem1  33790  breprexp  34597  bnj553  34861  bnj1253  34980  gonanegoal  35312  goalrlem  35356  goalr  35357  fmlasucdisj  35359  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  altopthsn  35922  bj-2upleq  36973  relowlpssretop  37325  iscrngo2  37964  extid  38271  cdleme18d  40262  fphpd  42777  oenassex  43280  rp-fakeuninass  43478  relexp0eq  43663  comptiunov2i  43668  clsk1indlem1  44007  ntrclskb  44031  onfrALTlem5  44505  onfrALTlem4  44506  onfrALTlem5VD  44847  onfrALTlem4VD  44848  dvnprodlem3  45919  sge0xadd  46406  reuabaiotaiota  47061  rrx2linest  48704  fucofvalne  49287