![]() |
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 12310 | . 2 ⊢ 4 = (3 + 1) | |
2 | 1 | eqcomi 2734 | 1 ⊢ (3 + 1) = 4 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 (class class class)co 7419 1c1 11141 + caddc 11143 3c3 12301 4c4 12302 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-4 12310 |
This theorem is referenced by: 7t6e42 12823 8t5e40 12828 9t5e45 12835 fac4 14276 hash4 14402 s4len 14886 bpoly4 16039 2exp16 17063 43prm 17094 83prm 17095 317prm 17098 1259lem2 17104 1259lem3 17105 1259lem4 17106 1259lem5 17107 2503lem1 17109 2503lem2 17110 4001lem1 17113 4001lem2 17114 4001lem4 17116 4001prm 17117 binom4 26827 quartlem1 26834 log2ublem3 26925 log2ub 26926 bclbnd 27258 addsqnreup 27421 tgcgr4 28407 upgr4cycl4dv4e 30067 ex-opab 30314 ex-ind-dvds 30343 fib4 34155 fib5 34156 hgt750lem 34414 hgt750lem2 34415 3lexlogpow5ineq1 41657 3lexlogpow5ineq5 41663 aks4d1p1p5 41678 aks4d1p1 41679 235t711 42002 3cubeslem3l 42248 3cubeslem3r 42249 inductionexd 43727 lhe4.4ex1a 43908 stoweidlem26 45552 stoweidlem34 45560 smfmullem2 46318 fmtno5lem4 47033 fmtno5 47034 fmtno5faclem2 47057 3ndvds4 47072 139prmALT 47073 31prm 47074 m5prm 47075 11t31e341 47209 2exp340mod341 47210 8exp8mod9 47213 sbgoldbalt 47258 sbgoldbo 47264 nnsum3primesle9 47271 nnsum4primeseven 47277 nnsum4primesevenALTV 47278 ackval3 47942 ackval3012 47951 ackval41a 47953 ackval41 47954 ackval42 47955 |
Copyright terms: Public domain | W3C validator |