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

Theorem 2p1e3 9052
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 8979 . 2  |-  3  =  ( 2  +  1 )
21eqcomi 2181 1  |-  ( 2  +  1 )  =  3
Colors of variables: wff set class
Syntax hints:    = wceq 1353  (class class class)co 5875   1c1 7812    + caddc 7814   2c2 8970   3c3 8971
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 1447  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-3 8979
This theorem is referenced by:  1p2e3  9053  cnm2m1cnm3  9170  6t5e30  9490  7t5e35  9495  8t4e32  9500  9t4e36  9507  decbin3  9525  halfthird  9526  fz0to3un2pr  10123  m1modge3gt1  10371  fac3  10712  hash3  10793  nn0o1gt2  11910  flodddiv4  11939  2lgsoddprmlem3c  14460
  Copyright terms: Public domain W3C validator