Theorem eqeq12iOLD 1898

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

Hypotheses

Ref	Expression
eqeq12i.1	|- A = B
eqeq12i.2	|- C = D

Assertion

Ref	Expression
eqeq12iOLD	|- (A = C <-> B = D)

Proof of Theorem eqeq12iOLD

Step	Hyp	Ref	Expression
1		eqeq12i.1	. . 3 |- A = B
2	1	eqeq1i 1891	. 2 |- (A = C <-> B = C)
3		eqeq12i.2	. . 3 |- C = D
4	3	eqeq2i 1894	. 2 |- (B = C <-> B = D)
5	2, 4	bitri 190	1 |- (A = C <-> B = D)

Syntax hints:   <-> wb 163   = wceq 1298

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain