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  4277  vn0  4338  sbceqg  4409  sbceqi  4410  preq2b  4848  preqr2  4850  otth  5484  otthg  5485  rncoeq  5973  fresaunres1  6762  eqfnov  7535  mpo2eqb  7538  f1o2ndf1  8105  fprlem1  8282  wfrlem5OLD  8310  ecopovsym  8810  frrlem15  9749  karden  9887  adderpqlem  10946  mulerpqlem  10947  addcmpblnr  11061  ax1ne0  11152  addrid  11391  sq11i  14152  nn0opth2i  14228  oppgcntz  19226  islpir  20880  evlsval  21641  volfiniun  25056  dvmptfsum  25484  sltval2  27149  sltsolem1  27168  nosepnelem  27172  nolt02o  27188  axlowdimlem13  28202  usgredg2v  28474  issubgr  28518  clwlkcompbp  29029  pjneli  30964  indifbi  31746  madjusmdetlem1  32796  breprexp  33634  bnj553  33898  bnj1253  34017  gonanegoal  34332  goalrlem  34376  goalr  34377  fmlasucdisj  34379  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  altopthsn  34922  bj-2upleq  35882  relowlpssretop  36234  iscrngo2  36854  extid  37168  cdleme18d  39155  fphpd  41540  oenassex  42054  rp-fakeuninass  42253  relexp0eq  42438  comptiunov2i  42443  clsk1indlem1  42782  ntrclskb  42806  onfrALTlem5  43289  onfrALTlem4  43290  onfrALTlem5VD  43632  onfrALTlem4VD  43633  dvnprodlem3  44651  sge0xadd  45138  reuabaiotaiota  45782  rrx2linest  47382