![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 6p3e9 | Structured version Visualization version GIF version |
Description: 6 + 3 = 9. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
6p3e9 | ⊢ (6 + 3) = 9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 11551 | . . . 4 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7030 | . . 3 ⊢ (6 + 3) = (6 + (2 + 1)) |
3 | 6cn 11578 | . . . 4 ⊢ 6 ∈ ℂ | |
4 | 2cn 11562 | . . . 4 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10444 | . . . 4 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | addassi 10500 | . . 3 ⊢ ((6 + 2) + 1) = (6 + (2 + 1)) |
7 | 2, 6 | eqtr4i 2821 | . 2 ⊢ (6 + 3) = ((6 + 2) + 1) |
8 | df-9 11557 | . . 3 ⊢ 9 = (8 + 1) | |
9 | 6p2e8 11646 | . . . 4 ⊢ (6 + 2) = 8 | |
10 | 9 | oveq1i 7029 | . . 3 ⊢ ((6 + 2) + 1) = (8 + 1) |
11 | 8, 10 | eqtr4i 2821 | . 2 ⊢ 9 = ((6 + 2) + 1) |
12 | 7, 11 | eqtr4i 2821 | 1 ⊢ (6 + 3) = 9 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 (class class class)co 7019 1c1 10387 + caddc 10389 2c2 11542 3c3 11543 6c6 11546 8c8 11548 9c9 11549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-ext 2768 ax-1cn 10444 ax-addcl 10446 ax-addass 10451 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-rex 3110 df-rab 3113 df-v 3438 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-br 4965 df-iota 6192 df-fv 6236 df-ov 7022 df-2 11550 df-3 11551 df-4 11552 df-5 11553 df-6 11554 df-7 11555 df-8 11556 df-9 11557 |
This theorem is referenced by: 3t3e9 11654 6p4e10 12020 2exp8 16252 139prm 16286 2503lem2 16300 4001lem1 16303 4001lem2 16304 4001lem4 16306 log2ublem3 25208 ex-gcd 27920 hgt750lem2 31532 kur14lem8 32062 problem5 32514 fmtno5lem1 43211 139prmALT 43255 gboge9 43425 gbpart9 43430 nnsum4primeseven 43461 |
Copyright terms: Public domain | W3C validator |