Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1p2e3 | Structured version Visualization version GIF version |
Description: 1 + 2 = 3. For a shorter proof using addcomli 11053, see 1p2e3ALT 12003. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 12-Dec-2022.) |
Ref | Expression |
---|---|
1p2e3 | ⊢ (1 + 2) = 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 11922 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7245 | . 2 ⊢ (1 + 2) = (1 + (1 + 1)) |
3 | ax-1cn 10816 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 3, 3, 3 | addassi 10872 | . 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1)) |
5 | 1p1e2 11984 | . . . 4 ⊢ (1 + 1) = 2 | |
6 | 5 | oveq1i 7244 | . . 3 ⊢ ((1 + 1) + 1) = (2 + 1) |
7 | 2p1e3 12001 | . . 3 ⊢ (2 + 1) = 3 | |
8 | 6, 7 | eqtri 2767 | . 2 ⊢ ((1 + 1) + 1) = 3 |
9 | 2, 4, 8 | 3eqtr2i 2773 | 1 ⊢ (1 + 2) = 3 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 (class class class)co 7234 1c1 10759 + caddc 10761 2c2 11914 3c3 11915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2710 ax-1cn 10816 ax-addass 10823 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4456 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4836 df-br 5070 df-iota 6358 df-fv 6408 df-ov 7237 df-2 11922 df-3 11923 |
This theorem is referenced by: fzo1to4tp 13359 binom3 13823 3lcm2e6woprm 16204 prmgaplem7 16642 2exp16 16676 prmlem1a 16692 23prm 16704 prmlem2 16705 83prm 16708 139prm 16709 163prm 16710 317prm 16711 631prm 16712 1259lem4 16719 1259prm 16721 2503lem2 16723 2503lem3 16724 4001lem2 16727 quart1lem 25769 log2ublem3 25862 log2ub 25863 pntibndlem2 26503 1kp2ke3k 28560 ex-ind-dvds 28575 fib4 32114 2np3bcnp1 39863 2xp3dxp2ge1d 39925 ex-decpmul 40075 sn-0ne2 40144 3cubeslem3r 40259 rabren3dioph 40387 fmtno4nprmfac193 44744 139prmALT 44766 127prm 44769 nnsum4primesodd 44966 nnsum4primesoddALTV 44967 ackval1012 45754 |
Copyright terms: Public domain | W3C validator |