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 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 2708

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

This theorem is referenced by:  neeq12i  2998  rabbi  3419  unineq  4228  vn0  4285  sbceqg  4352  sbceqi  4353  preq2b  4790  preqr2  4792  otth  5437  otthg  5438  rncoeq  5937  fresaunres1  6713  eqfnov  7496  mpo2eqb  7499  f1o2ndf1  8072  fprlem1  8250  ecopovsym  8766  frrlem15  9681  karden  9819  adderpqlem  10877  mulerpqlem  10878  addcmpblnr  10992  ax1ne0  11083  addrid  11326  sq11i  14153  nn0opth2i  14233  oppgcntz  19339  opprdomnb  20694  isdomn4r  20696  islpir  21326  evlsval  22064  volfiniun  25514  dvmptfsum  25942  ltsval2  27620  ltssolem1  27639  nosepnelem  27643  nolt02o  27659  axlowdimlem13  29023  usgredg2v  29296  issubgr  29340  clwlkcompbp  29850  pjneli  31794  indifbi  32590  madjusmdetlem1  33971  breprexp  34777  bnj553  35040  bnj1253  35159  gonanegoal  35534  goalrlem  35578  goalr  35579  fmlasucdisj  35581  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  altopthsn  36143  bj-2upleq  37319  relowlpssretop  37680  iscrngo2  38318  extid  38637  cdleme18d  40741  fphpd  43244  oenassex  43746  rp-fakeuninass  43943  relexp0eq  44128  comptiunov2i  44133  clsk1indlem1  44472  ntrclskb  44496  onfrALTlem5  44969  onfrALTlem4  44970  onfrALTlem5VD  45311  onfrALTlem4VD  45312  dvnprodlem3  46376  sge0xadd  46863  reuabaiotaiota  47535  rrx2linest  49218  fucofvalne  49800