|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 4p1e5 | Structured version Visualization version GIF version | ||
| Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.) | 
| Ref | Expression | 
|---|---|
| 4p1e5 | ⊢ (4 + 1) = 5 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-5 12333 | . 2 ⊢ 5 = (4 + 1) | |
| 2 | 1 | eqcomi 2745 | 1 ⊢ (4 + 1) = 5 | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 (class class class)co 7432 1c1 11157 + caddc 11159 4c4 12324 5c5 12325 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-cleq 2728 df-5 12333 | 
| This theorem is referenced by: 8t7e56 12855 9t6e54 12861 s5len 14940 bpoly4 16096 2exp16 17129 prmlem2 17158 163prm 17163 317prm 17164 631prm 17165 1259lem1 17169 1259lem2 17170 1259lem3 17171 1259lem4 17172 2503lem1 17175 2503lem2 17176 2503lem3 17177 4001lem1 17179 4001lem2 17180 4001lem3 17181 4001lem4 17182 log2ublem3 26992 log2ub 26993 ex-exp 30470 ex-fac 30471 fib5 34408 fib6 34409 hgt750lemd 34664 hgt750lem2 34668 60gcd7e1 42007 3lexlogpow5ineq1 42056 3lexlogpow5ineq5 42062 aks4d1p1p4 42073 aks4d1p1p7 42076 aks4d1p1 42078 5bc2eq10 42144 2ap1caineq 42147 sq45 42686 3cubeslem3l 42702 3cubeslem3r 42703 fmtno1 47533 257prm 47553 fmtno4prmfac 47564 fmtno4nprmfac193 47566 fmtno5faclem2 47572 31prm 47589 127prm 47591 m11nprm 47593 2exp340mod341 47725 nnsum3primesle9 47786 5m4e1 49371 | 
| Copyright terms: Public domain | W3C validator |