Theorem eq2tri

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

	Ref	Expression
Hypotheses	eq2tri.1	⊢ ( 𝐴 = 𝐶 → 𝐷 = 𝐹 )
	eq2tri.2	⊢ ( 𝐵 = 𝐷 → 𝐶 = 𝐺 )
Assertion	eq2tri	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐹 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐴 = 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eq2tri.1	⊢ ( 𝐴 = 𝐶 → 𝐷 = 𝐹 )
2		eq2tri.2	⊢ ( 𝐵 = 𝐷 → 𝐶 = 𝐺 )
3		ancom	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐴 = 𝐶 ) )
4	1	eqeq2d	⊢ ( 𝐴 = 𝐶 → ( 𝐵 = 𝐷 ↔ 𝐵 = 𝐹 ) )
5	4	pm5.32i	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐹 ) )
6	2	eqeq2d	⊢ ( 𝐵 = 𝐷 → ( 𝐴 = 𝐶 ↔ 𝐴 = 𝐺 ) )
7	6	pm5.32i	⊢ ( ( 𝐵 = 𝐷 ∧ 𝐴 = 𝐶 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐴 = 𝐺 ) )
8	3 5 7	3bitr3i	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐹 ) ↔ ( 𝐵 = 𝐷 ∧ 𝐴 = 𝐺 ) )