Theorem 4t3e12

Description: 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	4t3e12	⊢ ( 4 · 3 ) = ; 1 2

Proof

Step	Hyp	Ref	Expression
1		4nn0	⊢ 4 ∈ ℕ0
2		2nn0	⊢ 2 ∈ ℕ0
3		df-3	⊢ 3 = ( 2 + 1 )
4		4t2e8	⊢ ( 4 · 2 ) = 8
5		8p4e12	⊢ ( 8 + 4 ) = ; 1 2
6	1 2 3 4 5	4t3lem	⊢ ( 4 · 3 ) = ; 1 2