| 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 12331 | . 2 ⊢ 4 = (3 + 1) | |
| 2 | 1 | eqcomi 2746 | 1 ⊢ (3 + 1) = 4 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 (class class class)co 7431 1c1 11156 + caddc 11158 3c3 12322 4c4 12323 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-4 12331 |
| This theorem is referenced by: 7t6e42 12846 8t5e40 12851 9t5e45 12858 fz0to4untppr 13670 fz0to5un2tp 13671 fac4 14320 hash4 14446 hash7g 14525 s4len 14938 bpoly4 16095 2exp16 17128 43prm 17159 83prm 17160 317prm 17163 1259lem2 17169 1259lem3 17170 1259lem4 17171 1259lem5 17172 2503lem1 17174 2503lem2 17175 4001lem1 17178 4001lem2 17179 4001lem4 17181 4001prm 17182 binom4 26893 quartlem1 26900 log2ublem3 26991 log2ub 26992 bclbnd 27324 addsqnreup 27487 tgcgr4 28539 upgr4cycl4dv4e 30204 ex-opab 30451 ex-ind-dvds 30480 evl1deg3 33603 fib4 34406 fib5 34407 hgt750lem 34666 hgt750lem2 34667 3lexlogpow5ineq1 42055 3lexlogpow5ineq5 42061 aks4d1p1p5 42076 aks4d1p1 42077 235t711 42339 3cubeslem3l 42697 3cubeslem3r 42698 inductionexd 44168 lhe4.4ex1a 44348 stoweidlem26 46041 stoweidlem34 46049 smfmullem2 46807 fmtno5lem4 47543 fmtno5 47544 fmtno5faclem2 47567 3ndvds4 47582 139prmALT 47583 31prm 47584 m5prm 47585 11t31e341 47719 2exp340mod341 47720 8exp8mod9 47723 sbgoldbalt 47768 sbgoldbo 47774 nnsum3primesle9 47781 nnsum4primeseven 47787 nnsum4primesevenALTV 47788 2ltceilhalf 48015 ackval3 48604 ackval3012 48613 ackval41a 48615 ackval41 48616 ackval42 48617 |
| Copyright terms: Public domain | W3C validator |