eq2tri

Description: A compound transitive inference for class equality. (Contributed by NM, 22-Jan-2004)

	Ref	Expression
Hypotheses	eq2tri.1	$⊢ A = C \to D = F$
	eq2tri.2	$⊢ B = D \to C = G$
Assertion	eq2tri	$⊢ (A = C \land B = F) \leftrightarrow (B = D \land A = G)$

Step	Hyp	Ref	Expression
1		eq2tri.1	$⊢ A = C \to D = F$
2		eq2tri.2	$⊢ B = D \to C = G$
3		ancom	$⊢ (A = C \land B = D) \leftrightarrow (B = D \land A = C)$
4	1	eqeq2d	$⊢ A = C \to (B = D \leftrightarrow B = F)$
5	4	pm5.32i	$⊢ (A = C \land B = D) \leftrightarrow (A = C \land B = F)$
6	2	eqeq2d	$⊢ B = D \to (A = C \leftrightarrow A = G)$
7	6	pm5.32i	$⊢ (B = D \land A = C) \leftrightarrow (B = D \land A = G)$
8	3 5 7	3bitr3i	$⊢ (A = C \land B = F) \leftrightarrow (B = D \land A = G)$

Metamath Proof Explorer