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 11781 | . . 3 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7182 | . 2 ⊢ (3 · 3) = (3 · (2 + 1)) |
3 | 3cn 11798 | . . . . 5 ⊢ 3 ∈ ℂ | |
4 | 2cn 11792 | . . . . 5 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10674 | . . . . 5 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | adddii 10732 | . . . 4 ⊢ (3 · (2 + 1)) = ((3 · 2) + (3 · 1)) |
7 | 3t2e6 11883 | . . . . 5 ⊢ (3 · 2) = 6 | |
8 | 3t1e3 11882 | . . . . 5 ⊢ (3 · 1) = 3 | |
9 | 7, 8 | oveq12i 7183 | . . . 4 ⊢ ((3 · 2) + (3 · 1)) = (6 + 3) |
10 | 6, 9 | eqtri 2761 | . . 3 ⊢ (3 · (2 + 1)) = (6 + 3) |
11 | 6p3e9 11877 | . . 3 ⊢ (6 + 3) = 9 | |
12 | 10, 11 | eqtri 2761 | . 2 ⊢ (3 · (2 + 1)) = 9 |
13 | 2, 12 | eqtri 2761 | 1 ⊢ (3 · 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 (class class class)co 7171 1c1 10617 + caddc 10619 · cmul 10621 2c2 11772 3c3 11773 6c6 11776 9c9 11779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 ax-resscn 10673 ax-1cn 10674 ax-icn 10675 ax-addcl 10676 ax-mulcl 10678 ax-mulcom 10680 ax-addass 10681 ax-mulass 10682 ax-distr 10683 ax-1rid 10686 ax-cnre 10689 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-v 3400 df-un 3849 df-in 3851 df-ss 3861 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-iota 6298 df-fv 6348 df-ov 7174 df-2 11780 df-3 11781 df-4 11782 df-5 11783 df-6 11784 df-7 11785 df-8 11786 df-9 11787 |
This theorem is referenced by: sq3 13654 3dvds 15777 3dvdsdec 15778 3dvds2dec 15779 9nprm 16550 11prm 16552 43prm 16559 83prm 16560 317prm 16563 1259lem2 16569 1259lem4 16571 1259prm 16573 2503lem2 16575 mcubic 25585 log2tlbnd 25683 log2ublem3 25686 log2ub 25687 bposlem9 26028 lgsdir2lem5 26065 ex-lcm 28395 hgt750lem 32201 hgt750lem2 32202 3lexlogpow2ineq2 39684 3lexlogpow5ineq5 39685 3cubeslem3l 40072 3cubeslem3r 40073 inductionexd 41303 fmtno5lem3 44533 fmtno4prmfac193 44551 fmtno4nprmfac193 44552 127prm 44577 2exp340mod341 44711 9fppr8 44715 |
Copyright terms: Public domain | W3C validator |