![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3t2e6 | Structured version Visualization version GIF version |
Description: 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.) |
Ref | Expression |
---|---|
3t2e6 | ⊢ (3 · 2) = 6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3cn 11456 | . . 3 ⊢ 3 ∈ ℂ | |
2 | 1 | times2i 11521 | . 2 ⊢ (3 · 2) = (3 + 3) |
3 | 3p3e6 11534 | . 2 ⊢ (3 + 3) = 6 | |
4 | 2, 3 | eqtri 2802 | 1 ⊢ (3 · 2) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 (class class class)co 6922 + caddc 10275 · cmul 10277 2c2 11430 3c3 11431 6c6 11434 |
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-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-mulcl 10334 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-1rid 10342 ax-cnre 10345 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 df-2 11438 df-3 11439 df-4 11440 df-5 11441 df-6 11442 |
This theorem is referenced by: 3t3e9 11549 8th4div3 11602 halfpm6th 11603 halfthird 11990 fac3 13385 bpoly3 15191 bpoly4 15192 sin01bnd 15317 3lcm2e6woprm 15734 3lcm2e6 15844 prmo3 16149 2exp6 16194 6nprm 16215 7prm 16216 17prm 16222 37prm 16226 83prm 16228 163prm 16230 317prm 16231 631prm 16232 1259lem3 16238 1259lem4 16239 1259lem5 16240 2503lem2 16243 4001lem1 16246 4001lem3 16248 4001prm 16250 sincos6thpi 24705 quart1 25034 log2ublem2 25126 log2ublem3 25127 log2ub 25128 basellem5 25263 basellem8 25266 cht3 25351 ppiublem1 25379 ppiub 25381 bclbnd 25457 bpos1 25460 bposlem8 25468 bposlem9 25469 2lgslem3d 25576 2lgsoddprmlem3d 25590 hgt750lem2 31332 problem4 32159 problem5 32160 pigt3 34027 lhe4.4ex1a 39484 stoweidlem13 41157 257prm 42494 127prm 42536 mod42tp1mod8 42540 6even 42645 2t6m3t4e0 43141 zlmodzxzequa 43300 |
Copyright terms: Public domain | W3C validator |