| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 1p1e2 | GIF version | ||
| Description: 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
| Ref | Expression |
|---|---|
| 1p1e2 | ⊢ (1 + 1) = 2 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-2 9202 | . 2 ⊢ 2 = (1 + 1) | |
| 2 | 1 | eqcomi 2235 | 1 ⊢ (1 + 1) = 2 |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1397 (class class class)co 6018 1c1 8033 + caddc 8035 2c2 9194 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1495 ax-gen 1497 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-cleq 2224 df-2 9202 |
| This theorem is referenced by: 2m1e1 9261 add1p1 9394 sub1m1 9395 nn0n0n1ge2 9550 3halfnz 9577 10p10e20 9705 5t4e20 9712 6t4e24 9716 7t3e21 9720 8t3e24 9726 9t3e27 9733 fz0to3un2pr 10358 fldiv4p1lem1div2 10565 m1modge3gt1 10633 fac2 10993 hash2 11076 s2leng 11370 nn0o1gt2 12467 3lcm2e6woprm 12659 2exp8 13009 2exp11 13010 2exp16 13011 logbleb 15687 logblt 15688 1sgm2ppw 15721 1loopgrvd2fi 16158 2wlklem 16229 clwwlkext2edg 16275 ex-exp 16326 |
| Copyright terms: Public domain | W3C validator |