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

Theorem 2p1e3 9082
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 9009 . 2 3 = (2 + 1)
21eqcomi 2193 1 (2 + 1) = 3
Colors of variables: wff set class
Syntax hints:   = wceq 1364  (class class class)co 5896  1c1 7842   + caddc 7844  2c2 9000  3c3 9001
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 1458  ax-gen 1460  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-3 9009
This theorem is referenced by:  1p2e3  9083  cnm2m1cnm3  9200  6t5e30  9520  7t5e35  9525  8t4e32  9530  9t4e36  9537  decbin3  9555  halfthird  9556  fz0to3un2pr  10153  m1modge3gt1  10402  fac3  10744  hash3  10825  nn0o1gt2  11942  flodddiv4  11971  2lgsoddprmlem3c  14915
  Copyright terms: Public domain W3C validator