Theorem eqeq12i 2751

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

Syntax hints:   ↔ wb 205   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  neeq12i  3008  rabbi  3463  unineq  4278  vn0  4339  sbceqg  4410  sbceqi  4411  preq2b  4849  preqr2  4851  otth  5485  otthg  5486  rncoeq  5975  fresaunres1  6765  eqfnov  7538  mpo2eqb  7541  f1o2ndf1  8108  fprlem1  8285  wfrlem5OLD  8313  ecopovsym  8813  frrlem15  9752  karden  9890  adderpqlem  10949  mulerpqlem  10950  addcmpblnr  11064  ax1ne0  11155  addrid  11394  sq11i  14155  nn0opth2i  14231  oppgcntz  19231  islpir  20887  evlsval  21649  volfiniun  25064  dvmptfsum  25492  sltval2  27159  sltsolem1  27178  nosepnelem  27182  nolt02o  27198  axlowdimlem13  28212  usgredg2v  28484  issubgr  28528  clwlkcompbp  29039  pjneli  30976  indifbi  31758  madjusmdetlem1  32807  breprexp  33645  bnj553  33909  bnj1253  34028  gonanegoal  34343  goalrlem  34387  goalr  34388  fmlasucdisj  34390  satffunlem  34392  satffunlem1lem1  34393  satffunlem2lem1  34395  altopthsn  34933  bj-2upleq  35893  relowlpssretop  36245  iscrngo2  36865  extid  37179  cdleme18d  39166  fphpd  41554  oenassex  42068  rp-fakeuninass  42267  relexp0eq  42452  comptiunov2i  42457  clsk1indlem1  42796  ntrclskb  42820  onfrALTlem5  43303  onfrALTlem4  43304  onfrALTlem5VD  43646  onfrALTlem4VD  43647  dvnprodlem3  44664  sge0xadd  45151  reuabaiotaiota  45795  rrx2linest  47428