![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3p2e5 | Structured version Visualization version GIF version |
Description: 3 + 2 = 5. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
3p2e5 | ⊢ (3 + 2) = 5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 11501 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 6985 | . . . 4 ⊢ (3 + 2) = (3 + (1 + 1)) |
3 | 3cn 11519 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | ax-1cn 10391 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 10448 | . . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2798 | . . 3 ⊢ (3 + 2) = ((3 + 1) + 1) |
7 | df-4 11503 | . . . 4 ⊢ 4 = (3 + 1) | |
8 | 7 | oveq1i 6984 | . . 3 ⊢ (4 + 1) = ((3 + 1) + 1) |
9 | 6, 8 | eqtr4i 2798 | . 2 ⊢ (3 + 2) = (4 + 1) |
10 | df-5 11504 | . 2 ⊢ 5 = (4 + 1) | |
11 | 9, 10 | eqtr4i 2798 | 1 ⊢ (3 + 2) = 5 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1508 (class class class)co 6974 1c1 10334 + caddc 10336 2c2 11493 3c3 11494 4c4 11495 5c5 11496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 ax-1cn 10391 ax-addcl 10393 ax-addass 10398 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-rex 3087 df-rab 3090 df-v 3410 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-iota 6149 df-fv 6193 df-ov 6977 df-2 11501 df-3 11502 df-4 11503 df-5 11504 |
This theorem is referenced by: 3p3e6 11597 2exp16 16278 prmlem1a 16294 5prm 16296 prmlem2 16307 1259lem1 16318 1259lem4 16321 1259prm 16323 4001lem1 16328 4001lem4 16331 birthday 25249 ppiub 25497 bposlem6 25582 bposlem9 25585 2lgsoddprmlem3d 25706 ex-mod 28021 fib5 31341 hgt750lem2 31603 kur14lem8 32082 problem1 32465 235t711 38647 fmtnorec2 43107 fmtno5lem4 43120 257prm 43125 fmtno4nprmfac193 43138 2exp5 43157 41prothprmlem2 43185 linevalexample 43851 |
Copyright terms: Public domain | W3C validator |