![]() |
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 10568, see 1p2e3ALT 11526. (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 11438 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 6933 | . 2 ⊢ (1 + 2) = (1 + (1 + 1)) |
3 | ax-1cn 10330 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 3, 3, 3 | addassi 10387 | . 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1)) |
5 | 1p1e2 11507 | . . . 4 ⊢ (1 + 1) = 2 | |
6 | 5 | oveq1i 6932 | . . 3 ⊢ ((1 + 1) + 1) = (2 + 1) |
7 | 2p1e3 11524 | . . 3 ⊢ (2 + 1) = 3 | |
8 | 6, 7 | eqtri 2802 | . 2 ⊢ ((1 + 1) + 1) = 3 |
9 | 2, 4, 8 | 3eqtr2i 2808 | 1 ⊢ (1 + 2) = 3 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 (class class class)co 6922 1c1 10273 + caddc 10275 2c2 11430 3c3 11431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-1cn 10330 ax-addass 10337 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 df-2 11438 df-3 11439 |
This theorem is referenced by: fzo1to4tp 12875 binom3 13304 3lcm2e6woprm 15734 prmgaplem7 16165 2exp16 16196 prmlem1a 16212 23prm 16224 prmlem2 16225 83prm 16228 139prm 16229 163prm 16230 317prm 16231 631prm 16232 1259lem4 16239 1259prm 16241 2503lem2 16243 2503lem3 16244 4001lem2 16247 quart1lem 25033 log2ublem3 25127 log2ub 25128 pntibndlem2 25732 1kp2ke3k 27878 ex-ind-dvds 27893 fib4 31065 ex-decpmul 38160 rabren3dioph 38343 fmtno4nprmfac193 42511 139prmALT 42536 127prm 42540 nnsum4primesodd 42713 nnsum4primesoddALTV 42714 |
Copyright terms: Public domain | W3C validator |