Theorem eqeq12i 2758

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

Syntax hints:   ↔ wb 206   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  neeq12i  3013  rabbi  3475  unineq  4307  vn0  4368  sbceqg  4435  sbceqi  4436  preq2b  4872  preqr2  4874  otth  5504  otthg  5505  rncoeq  6002  fresaunres1  6794  eqfnov  7579  mpo2eqb  7582  f1o2ndf1  8163  fprlem1  8341  wfrlem5OLD  8369  ecopovsym  8877  frrlem15  9826  karden  9964  adderpqlem  11023  mulerpqlem  11024  addcmpblnr  11138  ax1ne0  11229  addrid  11470  sq11i  14240  nn0opth2i  14320  oppgcntz  19407  opprdomnb  20739  isdomn4r  20741  islpir  21361  evlsval  22133  volfiniun  25601  dvmptfsum  26033  sltval2  27719  sltsolem1  27738  nosepnelem  27742  nolt02o  27758  axlowdimlem13  28987  usgredg2v  29262  issubgr  29306  clwlkcompbp  29818  pjneli  31755  indifbi  32550  madjusmdetlem1  33773  breprexp  34610  bnj553  34874  bnj1253  34993  gonanegoal  35320  goalrlem  35364  goalr  35365  fmlasucdisj  35367  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  altopthsn  35925  bj-2upleq  36978  relowlpssretop  37330  iscrngo2  37957  extid  38266  cdleme18d  40252  fphpd  42772  oenassex  43280  rp-fakeuninass  43478  relexp0eq  43663  comptiunov2i  43668  clsk1indlem1  44007  ntrclskb  44031  onfrALTlem5  44513  onfrALTlem4  44514  onfrALTlem5VD  44856  onfrALTlem4VD  44857  dvnprodlem3  45869  sge0xadd  46356  reuabaiotaiota  47002  rrx2linest  48476