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  3436  unineq  4251  vn0  4308  sbceqg  4375  sbceqi  4376  preq2b  4811  preqr2  4813  otth  5444  otthg  5445  rncoeq  5943  fresaunres1  6733  eqfnov  7518  mpo2eqb  7521  f1o2ndf1  8101  fprlem1  8279  ecopovsym  8792  frrlem15  9710  karden  9848  adderpqlem  10907  mulerpqlem  10908  addcmpblnr  11022  ax1ne0  11113  addrid  11354  sq11i  14156  nn0opth2i  14236  oppgcntz  19296  opprdomnb  20626  isdomn4r  20628  islpir  21238  evlsval  21993  volfiniun  25448  dvmptfsum  25879  sltval2  27568  sltsolem1  27587  nosepnelem  27591  nolt02o  27607  axlowdimlem13  28881  usgredg2v  29154  issubgr  29198  clwlkcompbp  29712  pjneli  31652  indifbi  32449  madjusmdetlem1  33817  breprexp  34624  bnj553  34888  bnj1253  35007  gonanegoal  35339  goalrlem  35383  goalr  35384  fmlasucdisj  35386  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  altopthsn  35949  bj-2upleq  37000  relowlpssretop  37352  iscrngo2  37991  extid  38298  cdleme18d  40289  fphpd  42804  oenassex  43307  rp-fakeuninass  43505  relexp0eq  43690  comptiunov2i  43695  clsk1indlem1  44034  ntrclskb  44058  onfrALTlem5  44532  onfrALTlem4  44533  onfrALTlem5VD  44874  onfrALTlem4VD  44875  dvnprodlem3  45946  sge0xadd  46433  reuabaiotaiota  47085  rrx2linest  48728  fucofvalne  49311