Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3t3e9 | Structured version Visualization version GIF version |
Description: 3 times 3 equals 9. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
3t3e9 | ⊢ (3 · 3) = 9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 12037 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7286 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 12054 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 12048 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10929 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 10987 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 12139 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 12138 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 7287 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2766 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 12133 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2766 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2766 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 (class class class)co 7275 1c1 10872 + caddc 10874 · cmul 10876 2c2 12028 3c3 12029 6c6 12032 9c9 12035 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-mulcl 10933 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-1rid 10941 ax-cnre 10944 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-iota 6391 df-fv 6441 df-ov 7278 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 |
This theorem is referenced by: sq3 13915 3dvds 16040 3dvdsdec 16041 3dvds2dec 16042 9nprm 16814 11prm 16816 43prm 16823 83prm 16824 317prm 16827 1259lem2 16833 1259lem4 16835 1259prm 16837 2503lem2 16839 mcubic 25997 log2tlbnd 26095 log2ublem3 26098 log2ub 26099 bposlem9 26440 lgsdir2lem5 26477 ex-lcm 28822 hgt750lem 32631 hgt750lem2 32632 3lexlogpow2ineq2 40067 3lexlogpow5ineq5 40068 3cubeslem3l 40508 3cubeslem3r 40509 inductionexd 41765 fmtno5lem3 45007 fmtno4prmfac193 45025 fmtno4nprmfac193 45026 127prm 45051 2exp340mod341 45185 9fppr8 45189 |
Copyright terms: Public domain | W3C validator |