This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqtr3

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005) (Proof shortened by Wolf Lammen, 24-Oct-2024)

		Ref	Expression
	Assertion	eqtr3	$⊢ (A = C \land B = C) \to A = B$

Step	Hyp	Ref	Expression
1		eqeq2	$⊢ B = C \to (A = B \leftrightarrow A = C)$
2	1	biimparc	$⊢ (A = C \land B = C) \to A = B$