![]() |
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 12329 | . . 3 ⊢ 3 ∈ ℂ | |
2 | 1 | times2i 12387 | . 2 ⊢ (3 · 2) = (3 + 3) |
3 | 3p3e6 12400 | . 2 ⊢ (3 + 3) = 6 | |
4 | 2, 3 | eqtri 2755 | 1 ⊢ (3 · 2) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 (class class class)co 7424 + caddc 11147 · cmul 11149 2c2 12303 3c3 12304 6c6 12307 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-resscn 11201 ax-1cn 11202 ax-icn 11203 ax-addcl 11204 ax-mulcl 11206 ax-mulcom 11208 ax-addass 11209 ax-mulass 11210 ax-distr 11211 ax-1rid 11214 ax-cnre 11217 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-iota 6503 df-fv 6559 df-ov 7427 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 |
This theorem is referenced by: 3t3e9 12415 8th4div3 12468 halfpm6th 12469 halfthird 12856 fac3 14277 bpoly3 16040 bpoly4 16041 sin01bnd 16167 3lcm2e6woprm 16591 3lcm2e6 16709 prmo3 17015 2exp6 17061 6nprm 17084 7prm 17085 17prm 17091 37prm 17095 83prm 17097 163prm 17099 317prm 17100 631prm 17101 1259lem3 17107 1259lem4 17108 1259lem5 17109 2503lem2 17112 4001lem1 17115 4001lem3 17117 4001prm 17119 sincos6thpi 26468 pigt3 26470 quart1 26806 log2ublem2 26897 log2ublem3 26898 log2ub 26899 basellem5 27035 basellem8 27038 cht3 27123 ppiublem1 27153 ppiub 27155 bclbnd 27231 bpos1 27234 bposlem8 27242 bposlem9 27243 2lgslem3d 27350 2lgsoddprmlem3d 27364 hgt750lem2 34289 problem4 35277 problem5 35278 3exp7 41528 3cubeslem3l 42109 3cubeslem3r 42110 lhe4.4ex1a 43769 stoweidlem13 45403 257prm 46903 127prm 46941 mod42tp1mod8 46944 6even 47053 2exp340mod341 47075 2t6m3t4e0 47463 zlmodzxzequa 47615 |
Copyright terms: Public domain | W3C validator |