Theorem cleq12i 1114

Description: A useful inference for substituting definitions into an equality.

Hypotheses

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

Assertion

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

Proof of Theorem cleq12i

Step	Hyp	Ref	Expression
1		cleq12i.1	. . 3 ⊢ A = B
2	1	cleq1i 1108	. 2 ⊢ (A = C ↔ B = C)
3		cleq12i.2	. . 3 ⊢ C = D
4	3	cleq2i 1111	. 2 ⊢ (B = C ↔ B = D)
5	2, 4	bitr 151	1 ⊢ (A = C ↔ B = D)

Syntax hints:   ↔ wb 127   = wceq 1091

This theorem is referenced by:  unineq 1680  prer2 1873  opth 1898  rncoeq 2574  ecopoprsym 3246  karden 3551  mulcmpblnq 3847  addcmpblnr 3975  ax1ne0 4075  addcan2 4121  neg11 4164  div11 4252  rec11i 4261  cru 4529  sqe11 4702  nn0opth2 4725  sqr2irrlem4 4780  cjre 4811  pjnel 5665

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org