Metamath Proof Explorer


Theorem 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