![]() |
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 12272 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 7417 | . . . 4 ⊢ (3 + 2) = (3 + (1 + 1)) |
3 | 3cn 12290 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | ax-1cn 11165 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 11221 | . . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2764 | . . 3 ⊢ (3 + 2) = ((3 + 1) + 1) |
7 | df-4 12274 | . . . 4 ⊢ 4 = (3 + 1) | |
8 | 7 | oveq1i 7416 | . . 3 ⊢ (4 + 1) = ((3 + 1) + 1) |
9 | 6, 8 | eqtr4i 2764 | . 2 ⊢ (3 + 2) = (4 + 1) |
10 | df-5 12275 | . 2 ⊢ 5 = (4 + 1) | |
11 | 9, 10 | eqtr4i 2764 | 1 ⊢ (3 + 2) = 5 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 (class class class)co 7406 1c1 11108 + caddc 11110 2c2 12264 3c3 12265 4c4 12266 5c5 12267 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-1cn 11165 ax-addcl 11167 ax-addass 11172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6493 df-fv 6549 df-ov 7409 df-2 12272 df-3 12273 df-4 12274 df-5 12275 |
This theorem is referenced by: 3p3e6 12361 2exp5 17016 2exp16 17021 prmlem1a 17037 5prm 17039 prmlem2 17050 1259lem1 17061 1259lem4 17064 1259prm 17066 4001lem1 17071 4001lem4 17074 birthday 26449 ppiub 26697 bposlem6 26782 bposlem9 26785 2lgsoddprmlem3d 26906 ex-mod 29692 cyc3conja 32304 fib5 33393 hgt750lem2 33653 kur14lem8 34193 problem1 34639 235t711 41201 3cubeslem3l 41410 3cubeslem3r 41411 fmtnorec2 46198 fmtno5lem4 46211 257prm 46216 fmtno4nprmfac193 46229 41prothprmlem2 46273 linevalexample 47030 ackval2012 47331 ackval3012 47332 |
Copyright terms: Public domain | W3C validator |