Theorem eqeq12i 2754

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 2741	. 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)
3		eqeq12i.2	. . 3 ⊢ 𝐶 = 𝐷
4	3	eqeq2i 2749	. 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 2708

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

This theorem is referenced by:  neeq12i  2999  rabbi  3451  unineq  4268  vn0  4325  sbceqg  4392  sbceqi  4393  preq2b  4828  preqr2  4830  otth  5464  otthg  5465  rncoeq  5964  fresaunres1  6756  eqfnov  7541  mpo2eqb  7544  f1o2ndf1  8126  fprlem1  8304  wfrlem5OLD  8332  ecopovsym  8838  frrlem15  9776  karden  9914  adderpqlem  10973  mulerpqlem  10974  addcmpblnr  11088  ax1ne0  11179  addrid  11420  sq11i  14214  nn0opth2i  14294  oppgcntz  19352  opprdomnb  20682  isdomn4r  20684  islpir  21294  evlsval  22049  volfiniun  25505  dvmptfsum  25936  sltval2  27625  sltsolem1  27644  nosepnelem  27648  nolt02o  27664  axlowdimlem13  28938  usgredg2v  29211  issubgr  29255  clwlkcompbp  29769  pjneli  31709  indifbi  32506  madjusmdetlem1  33863  breprexp  34670  bnj553  34934  bnj1253  35053  gonanegoal  35379  goalrlem  35423  goalr  35424  fmlasucdisj  35426  satffunlem  35428  satffunlem1lem1  35429  satffunlem2lem1  35431  altopthsn  35984  bj-2upleq  37035  relowlpssretop  37387  iscrngo2  38026  extid  38333  cdleme18d  40319  fphpd  42806  oenassex  43309  rp-fakeuninass  43507  relexp0eq  43692  comptiunov2i  43697  clsk1indlem1  44036  ntrclskb  44060  onfrALTlem5  44534  onfrALTlem4  44535  onfrALTlem5VD  44876  onfrALTlem4VD  44877  dvnprodlem3  45944  sge0xadd  46431  reuabaiotaiota  47083  rrx2linest  48689  fucofvalne  49203