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

Metamath Proof Explorer

Theorem 2t1e2

Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018)

		Ref	Expression
	Assertion	2t1e2	$⊢ 2 \cdot 1 = 2$

Step	Hyp	Ref	Expression
1		2cn	$⊢ 2 \in ℂ$
2	1	mulridi	$⊢ 2 \cdot 1 = 2$