Theorem eqeq12i 2747

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  neeq12i  2991  rabbi  3425  unineq  4239  vn0  4296  sbceqg  4363  sbceqi  4364  preq2b  4798  preqr2  4800  otth  5427  otthg  5428  rncoeq  5923  fresaunres1  6697  eqfnov  7478  mpo2eqb  7481  f1o2ndf1  8055  fprlem1  8233  ecopovsym  8746  frrlem15  9653  karden  9791  adderpqlem  10848  mulerpqlem  10849  addcmpblnr  10963  ax1ne0  11054  addrid  11296  sq11i  14098  nn0opth2i  14178  oppgcntz  19243  opprdomnb  20602  isdomn4r  20604  islpir  21235  evlsval  21991  volfiniun  25446  dvmptfsum  25877  sltval2  27566  sltsolem1  27585  nosepnelem  27589  nolt02o  27605  axlowdimlem13  28899  usgredg2v  29172  issubgr  29216  clwlkcompbp  29727  pjneli  31667  indifbi  32464  madjusmdetlem1  33794  breprexp  34601  bnj553  34865  bnj1253  34984  gonanegoal  35325  goalrlem  35369  goalr  35370  fmlasucdisj  35372  satffunlem  35374  satffunlem1lem1  35375  satffunlem2lem1  35377  altopthsn  35935  bj-2upleq  36986  relowlpssretop  37338  iscrngo2  37977  extid  38284  cdleme18d  40274  fphpd  42789  oenassex  43291  rp-fakeuninass  43489  relexp0eq  43674  comptiunov2i  43679  clsk1indlem1  44018  ntrclskb  44042  onfrALTlem5  44516  onfrALTlem4  44517  onfrALTlem5VD  44858  onfrALTlem4VD  44859  dvnprodlem3  45929  sge0xadd  46416  reuabaiotaiota  47071  rrx2linest  48727  fucofvalne  49310