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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 | |
|
2 | 1 | oveq2i | |
3 | ax-1cn | |
|
4 | 3 3 3 | addassi | |
5 | 1p1e2 | |
|
6 | 5 | oveq1i | |
7 | 2p1e3 | |
|
8 | 6 7 | eqtri | |
9 | 2 4 8 | 3eqtr2i | |