Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
3t1e3
Next ⟩
3t2e6
Metamath Proof Explorer
Ascii
Structured
Theorem
3t1e3
Description:
3 times 1 equals 3.
(Contributed by
David A. Wheeler
, 8-Dec-2018)
Ref
Expression
Assertion
3t1e3
⊢
( 3 · 1 ) = 3
Proof
Step
Hyp
Ref
Expression
1
3cn
⊢
3 ∈ ℂ
2
1
mulid1i
⊢
( 3 · 1 ) = 3