Theorem eq2tri

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

	Ref	Expression
Hypotheses	eq2tri.1	|- ( A = C -> D = F )
	eq2tri.2	|- ( B = D -> C = G )
Assertion	eq2tri	|- ( ( A = C /\ B = F ) <-> ( B = D /\ A = G ) )

Proof

Step	Hyp	Ref	Expression
1		eq2tri.1	|- ( A = C -> D = F )
2		eq2tri.2	|- ( B = D -> C = G )
3		ancom	|- ( ( A = C /\ B = D ) <-> ( B = D /\ A = C ) )
4	1	eqeq2d	|- ( A = C -> ( B = D <-> B = F ) )
5	4	pm5.32i	|- ( ( A = C /\ B = D ) <-> ( A = C /\ B = F ) )
6	2	eqeq2d	|- ( B = D -> ( A = C <-> A = G ) )
7	6	pm5.32i	|- ( ( B = D /\ A = C ) <-> ( B = D /\ A = G ) )
8	3 5 7	3bitr3i	|- ( ( A = C /\ B = F ) <-> ( B = D /\ A = G ) )