![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3p1e4 | Structured version Visualization version GIF version |
Description: 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.) |
Ref | Expression |
---|---|
3p1e4 | ⊢ (3 + 1) = 4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 11293 | . 2 ⊢ 4 = (3 + 1) | |
2 | 1 | eqcomi 2769 | 1 ⊢ (3 + 1) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1632 (class class class)co 6814 1c1 10149 + caddc 10151 3c3 11283 4c4 11284 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-4 11293 |
This theorem is referenced by: 7t6e42 11864 8t5e40 11869 8t5e40OLD 11870 9t5e45 11878 fac4 13282 4bc3eq4 13329 hash4 13407 s4len 13864 bpoly4 15009 2exp16 16019 43prm 16051 83prm 16052 317prm 16055 prmo4 16057 1259lem2 16061 1259lem3 16062 1259lem4 16063 1259lem5 16064 2503lem1 16066 2503lem2 16067 4001lem1 16070 4001lem2 16071 4001lem4 16073 4001prm 16074 sincos6thpi 24487 binom4 24797 quartlem1 24804 log2ublem3 24895 log2ub 24896 bclbnd 25225 tgcgr4 25646 upgr4cycl4dv4e 27358 ex-opab 27621 ex-ind-dvds 27650 fib4 30796 fib5 30797 hgt750lem 31059 hgt750lem2 31060 inductionexd 38973 lhe4.4ex1a 39048 stoweidlem26 40764 stoweidlem34 40772 smfmullem2 41523 fmtno5lem4 41996 fmtno5 41997 fmtno5faclem2 42020 3ndvds4 42038 139prmALT 42039 31prm 42040 m5prm 42041 sbgoldbalt 42197 sbgoldbo 42203 nnsum3primesle9 42210 nnsum4primeseven 42216 nnsum4primesevenALTV 42217 |
Copyright terms: Public domain | W3C validator |