Theorem 2p1e3 9205

Description: 2 + 1 = 3. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
2p1e3	|- ( 2 + 1 ) = 3

Proof of Theorem 2p1e3

Step	Hyp	Ref	Expression
1		df-3 9131	. 2 |- 3 = ( 2 + 1 )
2	1	eqcomi 2211	1 |- ( 2 + 1 ) = 3

Syntax hints:   = wceq 1373  (class class class)co 5967   1c1 7961   + caddc 7963   2c2 9122   3c3 9123

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 1471  ax-gen 1473  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-3 9131

This theorem is referenced by:  1p2e3  9206  cnm2m1cnm3  9324  6t5e30  9645  7t5e35  9650  8t4e32  9655  9t4e36  9662  decbin3  9680  halfthird  9681  fz0to3un2pr  10280  m1modge3gt1  10553  fac3  10914  hash3  10995  nn0o1gt2  12331  flodddiv4  12362  3exp3  12876  2lgsoddprmlem3c  15701