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

Metamath Proof Explorer

Theorem xpeq12d

Description: Equality deduction for Cartesian product. (Contributed by NM, 8-Dec-2013)

Step	Hyp	Ref	Expression
1		xpeq1d.1	$⊢ φ \to A = B$
2		xpeq12d.2	$⊢ φ \to C = D$
3		xpeq12	$⊢ (A = B \land C = D) \to A \times C = B \times D$
4	1 2 3	syl2anc	$⊢ φ \to A \times C = B \times D$