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 11721 | . . 3 ⊢ 3 ∈ ℂ | |
2 | 1 | times2i 11779 | . 2 ⊢ (3 · 2) = (3 + 3) |
3 | 3p3e6 11792 | . 2 ⊢ (3 + 3) = 6 | |
4 | 2, 3 | eqtri 2846 | 1 ⊢ (3 · 2) = 6 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 (class class class)co 7158 + caddc 10542 · cmul 10544 2c2 11695 3c3 11696 6c6 11699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-mulcl 10601 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-1rid 10609 ax-cnre 10612 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-iota 6316 df-fv 6365 df-ov 7161 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 |
This theorem is referenced by: 3t3e9 11807 8th4div3 11860 halfpm6th 11861 halfthird 12244 fac3 13643 bpoly3 15414 bpoly4 15415 sin01bnd 15540 3lcm2e6woprm 15961 3lcm2e6 16074 prmo3 16379 2exp6 16424 6nprm 16445 7prm 16446 17prm 16452 37prm 16456 83prm 16458 163prm 16460 317prm 16461 631prm 16462 1259lem3 16468 1259lem4 16469 1259lem5 16470 2503lem2 16473 4001lem1 16476 4001lem3 16478 4001prm 16480 sincos6thpi 25103 pigt3 25105 quart1 25436 log2ublem2 25527 log2ublem3 25528 log2ub 25529 basellem5 25664 basellem8 25667 cht3 25752 ppiublem1 25780 ppiub 25782 bclbnd 25858 bpos1 25861 bposlem8 25869 bposlem9 25870 2lgslem3d 25977 2lgsoddprmlem3d 25991 hgt750lem2 31925 problem4 32913 problem5 32914 3cubeslem3l 39290 3cubeslem3r 39291 lhe4.4ex1a 40668 stoweidlem13 42305 257prm 43730 127prm 43770 mod42tp1mod8 43774 6even 43883 2exp340mod341 43905 2t6m3t4e0 44403 zlmodzxzequa 44558 |
Copyright terms: Public domain | W3C validator |