![]() |
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 11285 | . . 3 ⊢ 3 ∈ ℂ | |
2 | 1 | times2i 11338 | . 2 ⊢ (3 · 2) = (3 + 3) |
3 | 3p3e6 11351 | . 2 ⊢ (3 + 3) = 6 | |
4 | 2, 3 | eqtri 2780 | 1 ⊢ (3 · 2) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1630 (class class class)co 6811 + caddc 10129 · cmul 10131 2c2 11260 3c3 11261 6c6 11264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 ax-resscn 10183 ax-1cn 10184 ax-icn 10185 ax-addcl 10186 ax-addrcl 10187 ax-mulcl 10188 ax-mulrcl 10189 ax-mulcom 10190 ax-addass 10191 ax-mulass 10192 ax-distr 10193 ax-i2m1 10194 ax-1ne0 10195 ax-1rid 10196 ax-rrecex 10198 ax-cnre 10199 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ne 2931 df-ral 3053 df-rex 3054 df-rab 3057 df-v 3340 df-dif 3716 df-un 3718 df-in 3720 df-ss 3727 df-nul 4057 df-if 4229 df-sn 4320 df-pr 4322 df-op 4326 df-uni 4587 df-br 4803 df-iota 6010 df-fv 6055 df-ov 6814 df-2 11269 df-3 11270 df-4 11271 df-5 11272 df-6 11273 |
This theorem is referenced by: 3t3e9 11370 8th4div3 11442 halfpm6th 11443 halfthird 11875 fac3 13259 bpoly3 14986 bpoly4 14987 sin01bnd 15112 3lcm2e6woprm 15528 3lcm2e6 15640 prmo3 15945 2exp6 15995 6nprm 16016 7prm 16017 17prm 16024 37prm 16028 83prm 16030 163prm 16032 317prm 16033 631prm 16034 1259lem3 16040 1259lem4 16041 1259lem5 16042 2503lem2 16045 4001lem1 16048 4001lem3 16050 4001prm 16052 sincos6thpi 24464 quart1 24780 log2ublem2 24871 log2ublem3 24872 log2ub 24873 basellem5 25008 basellem8 25011 cht3 25096 ppiublem1 25124 ppiub 25126 bclbnd 25202 bpos1 25205 bposlem8 25213 bposlem9 25214 2lgslem3d 25321 2lgsoddprmlem3d 25335 hgt750lem2 31037 problem4 31867 problem5 31868 pigt3 33713 lhe4.4ex1a 39028 stoweidlem13 40731 257prm 41981 127prm 42023 mod42tp1mod8 42027 6even 42128 2t6m3t4e0 42634 zlmodzxzequa 42793 |
Copyright terms: Public domain | W3C validator |