Theorem 2p1e3 9190

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 9116	. 2 ⊢ 3 = (2 + 1)
2	1	eqcomi 2210	1 ⊢ (2 + 1) = 3

Syntax hints:   = wceq 1373  (class class class)co 5957  1c1 7946   + caddc 7948  2c2 9107  3c3 9108

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 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-3 9116

This theorem is referenced by:  1p2e3  9191  cnm2m1cnm3  9309  6t5e30  9630  7t5e35  9635  8t4e32  9640  9t4e36  9647  decbin3  9665  halfthird  9666  fz0to3un2pr  10265  m1modge3gt1  10538  fac3  10899  hash3  10980  nn0o1gt2  12291  flodddiv4  12322  3exp3  12836  2lgsoddprmlem3c  15661