Theorem 2p1e3 9170

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 9096	. 2 |- 3 = ( 2 + 1 )
2	1	eqcomi 2209	1 |- ( 2 + 1 ) = 3

Syntax hints:   = wceq 1373  (class class class)co 5944   1c1 7926   + caddc 7928   2c2 9087   3c3 9088

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 1470  ax-gen 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-3 9096

This theorem is referenced by:  1p2e3  9171  cnm2m1cnm3  9289  6t5e30  9610  7t5e35  9615  8t4e32  9620  9t4e36  9627  decbin3  9645  halfthird  9646  fz0to3un2pr  10245  m1modge3gt1  10516  fac3  10877  hash3  10958  nn0o1gt2  12216  flodddiv4  12247  3exp3  12761  2lgsoddprmlem3c  15586