![]() |
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 10821, see 1p2e3ALT 11769. (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 11688 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7146 | . 2 ⊢ (1 + 2) = (1 + (1 + 1)) |
3 | ax-1cn 10584 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 3, 3, 3 | addassi 10640 | . 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1)) |
5 | 1p1e2 11750 | . . . 4 ⊢ (1 + 1) = 2 | |
6 | 5 | oveq1i 7145 | . . 3 ⊢ ((1 + 1) + 1) = (2 + 1) |
7 | 2p1e3 11767 | . . 3 ⊢ (2 + 1) = 3 | |
8 | 6, 7 | eqtri 2821 | . 2 ⊢ ((1 + 1) + 1) = 3 |
9 | 2, 4, 8 | 3eqtr2i 2827 | 1 ⊢ (1 + 2) = 3 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 (class class class)co 7135 1c1 10527 + caddc 10529 2c2 11680 3c3 11681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-1cn 10584 ax-addass 10591 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 df-2 11688 df-3 11689 |
This theorem is referenced by: fzo1to4tp 13120 binom3 13581 3lcm2e6woprm 15949 prmgaplem7 16383 2exp16 16416 prmlem1a 16432 23prm 16444 prmlem2 16445 83prm 16448 139prm 16449 163prm 16450 317prm 16451 631prm 16452 1259lem4 16459 1259prm 16461 2503lem2 16463 2503lem3 16464 4001lem2 16467 quart1lem 25441 log2ublem3 25534 log2ub 25535 pntibndlem2 26175 1kp2ke3k 28231 ex-ind-dvds 28246 fib4 31772 2np3bcnp1 39348 2xp3dxp2ge1d 39387 ex-decpmul 39486 sn-0ne2 39544 3cubeslem3r 39628 rabren3dioph 39756 fmtno4nprmfac193 44091 139prmALT 44113 127prm 44116 nnsum4primesodd 44314 nnsum4primesoddALTV 44315 ackval1012 45104 |
Copyright terms: Public domain | W3C validator |