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 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

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

This theorem is referenced by:  neeq12i  3006  rabbi  3466  unineq  4287  vn0  4344  sbceqg  4411  sbceqi  4412  preq2b  4846  preqr2  4848  otth  5488  otthg  5489  rncoeq  5989  fresaunres1  6780  eqfnov  7563  mpo2eqb  7566  f1o2ndf1  8148  fprlem1  8326  wfrlem5OLD  8354  ecopovsym  8860  frrlem15  9798  karden  9936  adderpqlem  10995  mulerpqlem  10996  addcmpblnr  11110  ax1ne0  11201  addrid  11442  sq11i  14231  nn0opth2i  14311  oppgcntz  19384  opprdomnb  20718  isdomn4r  20720  islpir  21339  evlsval  22111  volfiniun  25583  dvmptfsum  26014  sltval2  27702  sltsolem1  27721  nosepnelem  27725  nolt02o  27741  axlowdimlem13  28970  usgredg2v  29245  issubgr  29289  clwlkcompbp  29803  pjneli  31743  indifbi  32540  madjusmdetlem1  33827  breprexp  34649  bnj553  34913  bnj1253  35032  gonanegoal  35358  goalrlem  35402  goalr  35403  fmlasucdisj  35405  satffunlem  35407  satffunlem1lem1  35408  satffunlem2lem1  35410  altopthsn  35963  bj-2upleq  37014  relowlpssretop  37366  iscrngo2  38005  extid  38312  cdleme18d  40298  fphpd  42832  oenassex  43336  rp-fakeuninass  43534  relexp0eq  43719  comptiunov2i  43724  clsk1indlem1  44063  ntrclskb  44087  onfrALTlem5  44567  onfrALTlem4  44568  onfrALTlem5VD  44910  onfrALTlem4VD  44911  dvnprodlem3  45968  sge0xadd  46455  reuabaiotaiota  47104  rrx2linest  48668  fucofvalne  49043