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 8924 | . 2 ⊢ 2 = (1 + 1) | |
2 | 1 | eqcomi 2174 | 1 ⊢ (1 + 1) = 2 |
Colors of variables: wff set class |
Syntax hints: = wceq 1348 (class class class)co 5850 1c1 7762 + caddc 7764 2c2 8916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-2 8924 |
This theorem is referenced by: 2m1e1 8983 add1p1 9114 sub1m1 9115 nn0n0n1ge2 9269 3halfnz 9296 10p10e20 9424 5t4e20 9431 6t4e24 9435 7t3e21 9439 8t3e24 9445 9t3e27 9452 fz0to3un2pr 10066 fldiv4p1lem1div2 10248 m1modge3gt1 10314 fac2 10652 hash2 10734 nn0o1gt2 11851 3lcm2e6woprm 12027 logbleb 13632 logblt 13633 ex-exp 13721 |
Copyright terms: Public domain | W3C validator |