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

Metamath Proof Explorer

Theorem xpeq12i

Description: Equality inference for Cartesian product. (Contributed by FL, 31-Aug-2009)

Step	Hyp	Ref	Expression
1		xpeq12i.1	$⊢ A = B$
2		xpeq12i.2	$⊢ C = D$
3		xpeq12	$⊢ (A = B \land C = D) \to A \times C = B \times D$
4	1 2 3	mp2an	$⊢ A \times C = B \times D$