Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 4p3e7 | Structured version Visualization version GIF version |
Description: 4 + 3 = 7. (Contributed by NM, 11-May-2004.) |
Ref | Expression |
---|---|
4p3e7 | ⊢ (4 + 3) = 7 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3 11899 | . . . 4 ⊢ 3 = (2 + 1) | |
2 | 1 | oveq2i 7229 | . . 3 ⊢ (4 + 3) = (4 + (2 + 1)) |
3 | 4cn 11920 | . . . 4 ⊢ 4 ∈ ℂ | |
4 | 2cn 11910 | . . . 4 ⊢ 2 ∈ ℂ | |
5 | ax-1cn 10792 | . . . 4 ⊢ 1 ∈ ℂ | |
6 | 3, 4, 5 | addassi 10848 | . . 3 ⊢ ((4 + 2) + 1) = (4 + (2 + 1)) |
7 | 2, 6 | eqtr4i 2768 | . 2 ⊢ (4 + 3) = ((4 + 2) + 1) |
8 | df-7 11903 | . . 3 ⊢ 7 = (6 + 1) | |
9 | 4p2e6 11988 | . . . 4 ⊢ (4 + 2) = 6 | |
10 | 9 | oveq1i 7228 | . . 3 ⊢ ((4 + 2) + 1) = (6 + 1) |
11 | 8, 10 | eqtr4i 2768 | . 2 ⊢ 7 = ((4 + 2) + 1) |
12 | 7, 11 | eqtr4i 2768 | 1 ⊢ (4 + 3) = 7 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 (class class class)co 7218 1c1 10735 + caddc 10737 2c2 11890 3c3 11891 4c4 11892 6c6 11894 7c7 11895 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-1cn 10792 ax-addcl 10794 ax-addass 10799 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3070 df-v 3415 df-dif 3874 df-un 3876 df-in 3878 df-ss 3888 df-nul 4243 df-if 4445 df-sn 4547 df-pr 4549 df-op 4553 df-uni 4825 df-br 5059 df-iota 6343 df-fv 6393 df-ov 7221 df-2 11898 df-3 11899 df-4 11900 df-5 11901 df-6 11902 df-7 11903 |
This theorem is referenced by: 4p4e8 11990 37prm 16679 317prm 16684 1259lem5 16693 2503lem2 16696 4001lem1 16699 4001lem2 16700 log2ub 25837 bposlem8 26177 2lgslem3d 26285 2lgsoddprmlem3d 26299 hgt750lem 32348 hgt750lem2 32349 fmtno5lem4 44689 257prm 44694 127prm 44732 gbpart7 44900 sbgoldbwt 44910 sbgoldbst 44911 ackval2012 45718 |
Copyright terms: Public domain | W3C validator |