This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Integer sets Some properties of specific numbers 1p2e3
Description: 1 + 2 = 3. For a shorter proof using addcomli , see 1p2e3ALT .
(Contributed by David A. Wheeler , 8-Dec-2018) Reduce dependencies on
axioms. (Revised by Steven Nguyen , 12-Dec-2022)
Ref
Expression
Assertion
1p2e3 ⊢ ( 1 + 2 ) = 3
Proof
Step
Hyp
Ref
Expression
1
df-2 ⊢ 2 = ( 1 + 1 )
2
1
oveq2i ⊢ ( 1 + 2 ) = ( 1 + ( 1 + 1 ) )
3
ax-1cn ⊢ 1 ∈ ℂ
4
3 3 3
addassi ⊢ ( ( 1 + 1 ) + 1 ) = ( 1 + ( 1 + 1 ) )
5
1p1e2 ⊢ ( 1 + 1 ) = 2
6
5
oveq1i ⊢ ( ( 1 + 1 ) + 1 ) = ( 2 + 1 )
7
2p1e3 ⊢ ( 2 + 1 ) = 3
8
6 7
eqtri ⊢ ( ( 1 + 1 ) + 1 ) = 3
9
2 4 8
3eqtr2i ⊢ ( 1 + 2 ) = 3