Theorem eqeq12i 2755

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

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  neeq12i  2999  rabbi  3431  unineq  4242  vn0  4299  sbceqg  4366  sbceqi  4367  preq2b  4805  preqr2  4807  otth  5440  otthg  5441  rncoeq  5939  fresaunres1  6715  eqfnov  7497  mpo2eqb  7500  f1o2ndf1  8074  fprlem1  8252  ecopovsym  8768  frrlem15  9681  karden  9819  adderpqlem  10877  mulerpqlem  10878  addcmpblnr  10992  ax1ne0  11083  addrid  11325  sq11i  14126  nn0opth2i  14206  oppgcntz  19305  opprdomnb  20662  isdomn4r  20664  islpir  21295  evlsval  22053  volfiniun  25516  dvmptfsum  25947  ltsval2  27636  ltssolem1  27655  nosepnelem  27659  nolt02o  27675  axlowdimlem13  29039  usgredg2v  29312  issubgr  29356  clwlkcompbp  29867  pjneli  31811  indifbi  32607  madjusmdetlem1  34005  breprexp  34811  bnj553  35074  bnj1253  35193  gonanegoal  35568  goalrlem  35612  goalr  35613  fmlasucdisj  35615  satffunlem  35617  satffunlem1lem1  35618  satffunlem2lem1  35620  altopthsn  36177  bj-2upleq  37260  relowlpssretop  37619  iscrngo2  38248  extid  38567  cdleme18d  40671  fphpd  43173  oenassex  43675  rp-fakeuninass  43872  relexp0eq  44057  comptiunov2i  44062  clsk1indlem1  44401  ntrclskb  44425  onfrALTlem5  44898  onfrALTlem4  44899  onfrALTlem5VD  45240  onfrALTlem4VD  45241  dvnprodlem3  46306  sge0xadd  46793  reuabaiotaiota  47447  rrx2linest  49102  fucofvalne  49684