![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2p1e3 | Structured version Visualization version GIF version |
Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
2p1e3 | ⊢ (2 + 1) = 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 11443 | . 2 ⊢ 3 = (2 + 1) | |
2 | 1 | eqcomi 2787 | 1 ⊢ (2 + 1) = 3 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 (class class class)co 6924 1c1 10275 + caddc 10277 2c2 11434 3c3 11435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-3 11443 |
This theorem is referenced by: 1p2e3 11529 1p2e3ALT 11530 cnm2m1cnm3 11639 6t5e30 11958 7t5e35 11963 8t4e32 11968 9t4e36 11975 decbin3 11993 halfthird 11994 fz0to3un2pr 12764 fzo0to42pr 12878 m1modge3gt1 13040 fac3 13389 hash3 13512 hashtplei 13584 hashtpg 13585 s3len 14049 repsw3 14106 bpoly3 15195 bpoly4 15196 nn0o1gt2 15515 flodddiv4 15547 3exp3 16201 13prm 16225 37prm 16230 43prm 16231 83prm 16232 139prm 16233 163prm 16234 317prm 16235 631prm 16236 1259lem1 16240 1259lem2 16241 1259lem3 16242 1259lem4 16243 1259lem5 16244 1259prm 16245 2503lem2 16247 2503prm 16249 4001lem1 16250 4001lem2 16251 4001lem4 16253 4001prm 16254 dcubic1lem 25025 dcubic2 25026 mcubic 25029 log2ublem3 25131 log2ub 25132 birthday 25137 chtub 25393 2lgsoddprmlem3c 25593 istrkg3ld 25816 usgr2wlkspthlem2 27114 elwwlks2ons3im 27338 umgrwwlks2on 27341 elwwlks2 27350 elwspths2spth 27351 clwwlknonex2lem1 27513 clwwlknonex2lem2 27514 3wlkdlem5 27570 3wlkdlem10 27576 upgr3v3e3cycl 27587 upgr4cycl4dv4e 27592 konigsberglem1 27662 konigsberglem2 27663 konigsberglem3 27664 numclwlk1 27803 frgrregord013 27831 ex-hash 27889 threehalves 30189 lmat22det 30490 fib3 31068 prodfzo03 31287 hgt750lemd 31332 hgt750lem 31335 hgt750lem2 31336 jm2.23 38532 lt3addmuld 40434 wallispilem4 41222 wallispi2lem1 41225 stirlinglem11 41238 fmtno0 42483 fmtno5lem4 42499 fmtno4prmfac 42515 fmtno4nprmfac193 42517 139prmALT 42542 31prm 42543 m7prm 42547 lighneallem4a 42556 41prothprmlem2 42566 sbgoldbalt 42704 bgoldbtbndlem1 42728 tgoldbachlt 42739 pgrpgt2nabl 43172 |
Copyright terms: Public domain | W3C validator |