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  3422  unineq  4235  vn0  4292  sbceqg  4359  sbceqi  4360  preq2b  4796  preqr2  4798  otth  5421  otthg  5422  rncoeq  5917  fresaunres1  6691  eqfnov  7469  mpo2eqb  7472  f1o2ndf1  8046  fprlem1  8224  ecopovsym  8737  frrlem15  9641  karden  9779  adderpqlem  10836  mulerpqlem  10837  addcmpblnr  10951  ax1ne0  11042  addrid  11284  sq11i  14086  nn0opth2i  14166  oppgcntz  19230  opprdomnb  20586  isdomn4r  20588  islpir  21219  evlsval  21975  volfiniun  25429  dvmptfsum  25860  sltval2  27549  sltsolem1  27568  nosepnelem  27572  nolt02o  27588  axlowdimlem13  28886  usgredg2v  29159  issubgr  29203  clwlkcompbp  29714  pjneli  31654  indifbi  32452  madjusmdetlem1  33808  breprexp  34614  bnj553  34878  bnj1253  34997  gonanegoal  35342  goalrlem  35386  goalr  35387  fmlasucdisj  35389  satffunlem  35391  satffunlem1lem1  35392  satffunlem2lem1  35394  altopthsn  35952  bj-2upleq  37003  relowlpssretop  37355  iscrngo2  37994  extid  38301  cdleme18d  40291  fphpd  42806  oenassex  43308  rp-fakeuninass  43506  relexp0eq  43691  comptiunov2i  43696  clsk1indlem1  44035  ntrclskb  44059  onfrALTlem5  44532  onfrALTlem4  44533  onfrALTlem5VD  44874  onfrALTlem4VD  44875  dvnprodlem3  45943  sge0xadd  46430  reuabaiotaiota  47085  rrx2linest  48741  fucofvalne  49324