Theorem eqeq12i 2782

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

Syntax hints:   ↔ wb 208   = wceq 1562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756

This theorem is referenced by:  neeq12i  3025  rabbi  3446  unineq  4242  vn0  4299  sbceqg  4368  sbceqi  4369  preq2b  4807  preqr2  4809  otth  5454  otthg  5455  rncoeq  5960  fresaunres1  6739  eqfnov  7527  mpo2eqb  7530  f1o2ndf1  8103  fprlem1  8283  ecopovsym  8803  frrlem15  9717  karden  9855  adderpqlem  10914  mulerpqlem  10915  addcmpblnr  11029  ax1ne0  11120  addrid  11365  sq11i  14206  nn0opth2i  14286  oppgcntz  19406  opprdomnb  20769  isdomn4r  20771  islpir  21400  evlsval  22141  volfiniun  25611  dvmptfsum  26039  ltsval2  27722  ltssolem1  27741  nosepnelem  27745  nolt02o  27761  axlowdimlem13  29157  usgredg2v  29430  issubgr  29474  clwlkcompbp  29984  pjneli  31928  indifbi  32721  madjusmdetlem1  34126  breprexp  34929  bnj553  35195  bnj1253  35314  gonanegoal  35707  goalrlem  35751  goalr  35752  fmlasucdisj  35754  satffunlem  35756  satffunlem1lem1  35757  satffunlem2lem1  35759  altopthsn  36316  bj-2upleq  37502  relowlpssretop  37863  iscrngo2  38501  extid  38820  cdleme18d  40924  fphpd  43398  oenassex  43900  rp-fakeuninass  44097  relexp0eq  44282  comptiunov2i  44287  clsk1indlem1  44626  ntrclskb  44650  onfrALTlem5  45123  onfrALTlem4  45124  onfrALTlem5VD  45465  onfrALTlem4VD  45466  dvnprodlem3  46527  sge0xadd  47014  reuabaiotaiota  47686  rrx2linest  49369  fucofvalne  49951