ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2p1e3 Unicode version

Theorem 2p1e3 9066
Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
2p1e3  |-  ( 2  +  1 )  =  3

Proof of Theorem 2p1e3
StepHypRef Expression
1 df-3 8993 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2191 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff set class
Syntax hints:    = wceq 1363  (class class class)co 5888   1c1 7826    + caddc 7828   2c2 8984   3c3 8985
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 1457  ax-gen 1459  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-3 8993
This theorem is referenced by:  1p2e3  9067  cnm2m1cnm3  9184  6t5e30  9504  7t5e35  9509  8t4e32  9514  9t4e36  9521  decbin3  9539  halfthird  9540  fz0to3un2pr  10137  m1modge3gt1  10385  fac3  10726  hash3  10807  nn0o1gt2  11924  flodddiv4  11953  2lgsoddprmlem3c  14753
  Copyright terms: Public domain W3C validator