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  28243  usgredg2v  28515  issubgr  28559  clwlkcompbp  29070  pjneli  31007  indifbi  31789  madjusmdetlem1  32838  breprexp  33676  bnj553  33940  bnj1253  34059  gonanegoal  34374  goalrlem  34418  goalr  34419  fmlasucdisj  34421  satffunlem  34423  satffunlem1lem1  34424  satffunlem2lem1  34426  altopthsn  34964  bj-2upleq  35941  relowlpssretop  36293  iscrngo2  36913  extid  37227  cdleme18d  39214  fphpd  41602  oenassex  42116  rp-fakeuninass  42315  relexp0eq  42500  comptiunov2i  42505  clsk1indlem1  42844  ntrclskb  42868  onfrALTlem5  43351  onfrALTlem4  43352  onfrALTlem5VD  43694  onfrALTlem4VD  43695  dvnprodlem3  44712  sge0xadd  45199  reuabaiotaiota  45843  rrx2linest  47476