Theorem eqeq12i 2778

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  neeq12i  3021  rabbi  3441  unineq  4233  vn0  4290  vn0OLD  4291  sbceqg  4369  sbceqi  4370  preq2b  4806  preqr2  4808  otth  5452  otthg  5453  rncoeq  5962  fresaunres1  6755  eqfnov  7549  mpo2eqb  7552  f1o2ndf1  8133  fprlem1  8318  ecopovsym  8840  frrlem15  9761  kardenOLD  9960  adderpqlem  11039  mulerpqlem  11040  addcmpblnr  11154  ax1ne0  11245  addrid  11490  sq11i  14334  nn0opth2i  14415  degenmgmnfn  19136  oppgcntz  19578  opprdomnb  20968  isdomn4r  20970  islpir  21652  evlsval  22395  volfiniun  25868  dvmptfsum  26295  ltsval2  28013  ltssolem1  28032  nosepnelem  28036  nolt02o  28052  axlowdimlem13  29532  usgredg2v  29808  issubgr  29852  clwlkcompbp  30369  pjneli  32325  indifbi  33158  madjusmdetlem1  34501  breprexp  35304  bnj553  35570  bnj1253  35689  gonanegoal  36159  goalrlem  36203  goalr  36204  fmlasucdisj  36206  satffunlem  36208  satffunlem1lem1  36209  satffunlem2lem1  36211  altopthsn  36768  bj-2upleq  37967  bj-vn0ALT  38029  relowlpssretop  38330  iscrngo2  38974  extid  39291  cdleme18d  41395  fphpd  43865  oenassex  44362  rp-fakeuninass  44559  relexp0eq  44743  comptiunov2i  44748  clsk1indlem1  45087  ntrclskb  45111  onfrALTlem5  45567  onfrALTlem4  45568  onfrALTlem5VD  45909  onfrALTlem4VD  45910  dvnprodlem3  47000  sge0xadd  47487  reuabaiotaiota  48199  rrx2linest  49896  fucofvalne  50475