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 10832, see 1p2e3ALT 11782. (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 11701 | . . 3 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7167 | . 2 ⊢ (1 + 2) = (1 + (1 + 1)) |
3 | ax-1cn 10595 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 3, 3, 3 | addassi 10651 | . 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1)) |
5 | 1p1e2 11763 | . . . 4 ⊢ (1 + 1) = 2 | |
6 | 5 | oveq1i 7166 | . . 3 ⊢ ((1 + 1) + 1) = (2 + 1) |
7 | 2p1e3 11780 | . . 3 ⊢ (2 + 1) = 3 | |
8 | 6, 7 | eqtri 2844 | . 2 ⊢ ((1 + 1) + 1) = 3 |
9 | 2, 4, 8 | 3eqtr2i 2850 | 1 ⊢ (1 + 2) = 3 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 (class class class)co 7156 1c1 10538 + caddc 10540 2c2 11693 3c3 11694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-1cn 10595 ax-addass 10602 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-iota 6314 df-fv 6363 df-ov 7159 df-2 11701 df-3 11702 |
This theorem is referenced by: fzo1to4tp 13126 binom3 13586 3lcm2e6woprm 15959 prmgaplem7 16393 2exp16 16424 prmlem1a 16440 23prm 16452 prmlem2 16453 83prm 16456 139prm 16457 163prm 16458 317prm 16459 631prm 16460 1259lem4 16467 1259prm 16469 2503lem2 16471 2503lem3 16472 4001lem2 16475 quart1lem 25433 log2ublem3 25526 log2ub 25527 pntibndlem2 26167 1kp2ke3k 28225 ex-ind-dvds 28240 fib4 31662 2xp3dxp2ge1d 39117 ex-decpmul 39198 sn-0ne2 39256 3cubeslem3r 39304 rabren3dioph 39432 fmtno4nprmfac193 43756 139prmALT 43779 127prm 43783 nnsum4primesodd 43981 nnsum4primesoddALTV 43982 |
Copyright terms: Public domain | W3C validator |