Theorem eqeq12i 2366

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
eqeq12i.1	⊢ A = B
eqeq12i.2	⊢ C = D

Assertion

Ref	Expression
eqeq12i	⊢ (A = C ↔ B = D)

Proof of Theorem eqeq12i

Step	Hyp	Ref	Expression
1		eqeq12i.1	. 2 ⊢ A = B
2		eqeq12i.2	. 2 ⊢ C = D
3		eqeq12 2365	. 2 ⊢ ((A = B ∧ C = D) → (A = C ↔ B = D))
4	1, 2, 3	mp2an 653	1 ⊢ (A = C ↔ B = D)

Syntax hints:   ↔ wb 176   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346

This theorem is referenced by:  rabbi  2790  sbceqg  3153  unineq  3506  preqr2  4126  opkthg  4132  preaddccan2  4456  ltfinirr  4458  addccan1  4561  rncoeq  4976  swapf1o  5512  eqfnov  5590  eqncg  6127  ncseqnc  6129  tc11  6229  taddc  6230  muc0or  6253  addccan2nc  6266  nnc3n3p1  6279