Theorem eqeq12i 2779

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

Syntax hints:   ↔ wb 209   = wceq 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753

This theorem is referenced by:  neeq12i  3022  rabbi  3444  unineq  4240  vn0  4297  vn0OLD  4298  sbceqg  4376  sbceqi  4377  preq2b  4811  preqr2  4813  otth  5466  otthg  5467  rncoeq  5971  fresaunres1  6751  eqfnov  7539  mpo2eqb  7542  f1o2ndf1  8116  fprlem1  8296  ecopovsym  8816  frrlem15  9728  karden  9880  adderpqlem  10938  mulerpqlem  10939  addcmpblnr  11053  ax1ne0  11144  addrid  11389  sq11i  14226  nn0opth2i  14306  oppgcntz  19433  opprdomnb  20800  isdomn4r  20802  islpir  21475  evlsval  22216  volfiniun  25685  dvmptfsum  26113  ltsval2  27796  ltssolem1  27815  nosepnelem  27819  nolt02o  27835  axlowdimlem13  29270  usgredg2v  29543  issubgr  29587  clwlkcompbp  30097  pjneli  32041  indifbi  32832  madjusmdetlem1  34183  breprexp  34986  bnj553  35252  bnj1253  35371  gonanegoal  35798  goalrlem  35842  goalr  35843  fmlasucdisj  35845  satffunlem  35847  satffunlem1lem1  35848  satffunlem2lem1  35850  altopthsn  36407  bj-2upleq  37592  bj-vn0ALT  37652  relowlpssretop  37954  iscrngo2  38592  extid  38911  cdleme18d  41015  fphpd  43491  oenassex  43993  rp-fakeuninass  44190  relexp0eq  44375  comptiunov2i  44380  clsk1indlem1  44719  ntrclskb  44743  onfrALTlem5  45199  onfrALTlem4  45200  onfrALTlem5VD  45541  onfrALTlem4VD  45542  dvnprodlem3  46610  sge0xadd  47097  reuabaiotaiota  47769  rrx2linest  49467  fucofvalne  50048