![]() |
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 11279 | . . . . 5 ⊢ 2 = (1 + 1) | |
2 | 1 | oveq2i 6802 | . . . 4 ⊢ (3 + 2) = (3 + (1 + 1)) |
3 | 3cn 11295 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | ax-1cn 10194 | . . . . 5 ⊢ 1 ∈ ℂ | |
5 | 3, 4, 4 | addassi 10248 | . . . 4 ⊢ ((3 + 1) + 1) = (3 + (1 + 1)) |
6 | 2, 5 | eqtr4i 2796 | . . 3 ⊢ (3 + 2) = ((3 + 1) + 1) |
7 | df-4 11281 | . . . 4 ⊢ 4 = (3 + 1) | |
8 | 7 | oveq1i 6801 | . . 3 ⊢ (4 + 1) = ((3 + 1) + 1) |
9 | 6, 8 | eqtr4i 2796 | . 2 ⊢ (3 + 2) = (4 + 1) |
10 | df-5 11282 | . 2 ⊢ 5 = (4 + 1) | |
11 | 9, 10 | eqtr4i 2796 | 1 ⊢ (3 + 2) = 5 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 (class class class)co 6791 1c1 10137 + caddc 10139 2c2 11270 3c3 11271 4c4 11272 5c5 11273 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-addass 10201 ax-i2m1 10204 ax-1ne0 10205 ax-rrecex 10208 ax-cnre 10209 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-iota 5992 df-fv 6037 df-ov 6794 df-2 11279 df-3 11280 df-4 11281 df-5 11282 |
This theorem is referenced by: 3p3e6 11361 2exp16 15997 prmlem1a 16013 5prm 16015 prmlem2 16027 1259lem1 16038 1259lem4 16041 1259prm 16043 4001lem1 16048 4001lem4 16051 birthday 24895 ppiub 25143 bposlem6 25228 bposlem9 25231 2lgsoddprmlem3d 25352 ex-mod 27641 fib5 30800 hgt750lem2 31063 kur14lem8 31526 problem1 31889 fmtnorec2 41976 fmtno5lem4 41989 257prm 41994 fmtno4nprmfac193 42007 2exp5 42028 41prothprmlem2 42056 linevalexample 42705 |
Copyright terms: Public domain | W3C validator |