Theorem eqeq12i 2778

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  neeq12i  3021  rabbi  3441  unineq  4234  vn0  4291  vn0OLD  4292  sbceqg  4370  sbceqi  4371  preq2b  4807  preqr2  4809  otth  5453  otthg  5454  rncoeq  5960  fresaunres1  6744  eqfnov  7538  mpo2eqb  7541  f1o2ndf1  8117  fprlem1  8297  ecopovsym  8819  frrlem15  9739  kardenOLD  9917  adderpqlem  10996  mulerpqlem  10997  addcmpblnr  11111  ax1ne0  11202  addrid  11447  sq11i  14288  nn0opth2i  14368  degenmgmnfn  19083  oppgcntz  19525  opprdomnb  20915  isdomn4r  20917  islpir  21599  evlsval  22342  volfiniun  25815  dvmptfsum  26242  ltsval2  27932  ltssolem1  27951  nosepnelem  27955  nolt02o  27971  axlowdimlem13  29451  usgredg2v  29727  issubgr  29771  clwlkcompbp  30288  pjneli  32244  indifbi  33035  madjusmdetlem1  34378  breprexp  35182  bnj553  35448  bnj1253  35567  gonanegoal  36032  goalrlem  36076  goalr  36077  fmlasucdisj  36079  satffunlem  36081  satffunlem1lem1  36082  satffunlem2lem1  36084  altopthsn  36642  bj-2upleq  37841  bj-vn0ALT  37901  relowlpssretop  38201  iscrngo2  38845  extid  39162  cdleme18d  41266  fphpd  43755  oenassex  44257  rp-fakeuninass  44454  relexp0eq  44639  comptiunov2i  44644  clsk1indlem1  44983  ntrclskb  45007  onfrALTlem5  45463  onfrALTlem4  45464  onfrALTlem5VD  45805  onfrALTlem4VD  45806  dvnprodlem3  46874  sge0xadd  47361  reuabaiotaiota  48073  rrx2linest  49770  fucofvalne  50349