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 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-2 | |- 2 = ( 1 + 1 ) |
|
| 2 | 1 | oveq2i | |- ( 1 + 2 ) = ( 1 + ( 1 + 1 ) ) |
| 3 | ax-1cn | |- 1 e. CC |
|
| 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 |