Theorem eqeq12i 2759

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

Syntax hints:   ↔ wb 208   = wceq 1548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733

This theorem is referenced by:  neeq12i  3002  rabbi  3423  unineq  4218  vn0  4275  sbceqg  4342  sbceqi  4343  preq2b  4780  preqr2  4782  otth  5426  otthg  5427  rncoeq  5930  fresaunres1  6703  eqfnov  7488  mpo2eqb  7491  f1o2ndf1  8063  fprlem1  8243  ecopovsym  8760  frrlem15  9676  karden  9814  adderpqlem  10873  mulerpqlem  10874  addcmpblnr  10988  ax1ne0  11079  addrid  11322  sq11i  14148  nn0opth2i  14228  oppgcntz  19333  opprdomnb  20692  isdomn4r  20694  islpir  21324  evlsval  22065  volfiniun  25535  dvmptfsum  25963  ltsval2  27640  ltssolem1  27659  nosepnelem  27663  nolt02o  27679  axlowdimlem13  29043  usgredg2v  29316  issubgr  29360  clwlkcompbp  29870  pjneli  31814  indifbi  32610  madjusmdetlem1  34021  breprexp  34827  bnj553  35093  bnj1253  35212  gonanegoal  35593  goalrlem  35637  goalr  35638  fmlasucdisj  35640  satffunlem  35642  satffunlem1lem1  35643  satffunlem2lem1  35645  altopthsn  36202  bj-2upleq  37378  relowlpssretop  37739  iscrngo2  38377  extid  38696  cdleme18d  40800  fphpd  43274  oenassex  43776  rp-fakeuninass  43973  relexp0eq  44158  comptiunov2i  44163  clsk1indlem1  44502  ntrclskb  44526  onfrALTlem5  44999  onfrALTlem4  45000  onfrALTlem5VD  45341  onfrALTlem4VD  45342  dvnprodlem3  46403  sge0xadd  46890  reuabaiotaiota  47562  rrx2linest  49245  fucofvalne  49827