Theorem 2p1e3 12045

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

Syntax hints:   = wceq 1539  (class class class)co 7255  1c1 10803   + caddc 10805  2c2 11958  3c3 11959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-3 11967

This theorem is referenced by:  1p2e3  12046  1p2e3ALT  12047  cnm2m1cnm3  12156  6t5e30  12473  7t5e35  12478  8t4e32  12483  9t4e36  12490  decbin3  12508  halfthird  12509  fz0to3un2pr  13287  fzo0to42pr  13402  m1modge3gt1  13566  fac3  13922  hash3  14049  hashtplei  14126  hashtpg  14127  s3len  14535  repsw3  14592  bpoly3  15696  bpoly4  15697  nn0o1gt2  16018  flodddiv4  16050  ge2nprmge4  16334  3exp3  16721  13prm  16745  37prm  16750  43prm  16751  83prm  16752  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem2  16767  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem4  16773  4001prm  16774  mcubic  25902  log2ublem3  26003  log2ub  26004  birthday  26009  chtub  26265  2lgsoddprmlem3c  26465  istrkg3ld  26726  usgr2wlkspthlem2  28027  elwwlks2ons3im  28220  umgrwwlks2on  28223  elwwlks2  28232  elwspths2spth  28233  clwwlknonex2lem1  28372  clwwlknonex2lem2  28373  3wlkdlem5  28428  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  numclwlk1  28636  frgrregord013  28660  ex-hash  28718  threehalves  31091  lmat22det  31674  fib3  32270  prodfzo03  32483  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  aks4d1p1p2  40006  aks4d1p1p7  40010  aks4d1p1  40012  2np3bcnp1  40028  3cubeslem3l  40424  3cubeslem3r  40425  jm2.23  40734  resqrtvalex  41142  lt3addmuld  42730  wallispilem4  43499  wallispi2lem1  43502  stirlinglem11  43515  fmtno0  44880  fmtno5lem4  44896  fmtno4prmfac  44912  fmtno4nprmfac193  44914  139prmALT  44936  31prm  44937  m7prm  44940  lighneallem4a  44948  41prothprmlem2  44958  2exp340mod341  45073  sbgoldbalt  45121  bgoldbtbndlem1  45145  tgoldbachlt  45156  pgrpgt2nabl  45590  ackval2  45916  ackval3  45917  ackval0012  45923  ackval3012  45926