Theorem 2p1e3 12309

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

Syntax hints:   = wceq 1542  (class class class)co 7360  1c1 11030   + caddc 11032  2c2 12227  3c3 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-3 12236

This theorem is referenced by:  1p2e3  12310  1p2e3ALT  12311  halfthird  12389  halfpm6th  12390  cnm2m1cnm3  12421  6t5e30  12742  7t5e35  12747  8t4e32  12752  9t4e36  12759  decbin3  12777  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  fzo0to42pr  13699  m1modge3gt1  13871  fac3  14233  hash3  14359  hashtplei  14437  hashtpg  14438  hash3tpexb  14447  s3len  14847  repsw3  14904  bpoly3  16014  bpoly4  16015  nn0o1gt2  16341  flodddiv4  16375  ge2nprmge4  16662  3exp3  17053  13prm  17077  37prm  17082  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem2  17099  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem4  17105  4001prm  17106  mcubic  26824  log2ublem3  26925  log2ub  26926  birthday  26931  chtub  27189  2lgsoddprmlem3c  27389  istrkg3ld  28543  usgr2wlkspthlem2  29841  elwwlks2ons3im  30037  usgrwwlks2on  30041  umgrwwlks2on  30042  elwwlks2  30052  elwspths2spth  30053  clwwlknonex2lem1  30192  clwwlknonex2lem2  30193  3wlkdlem5  30248  3wlkdlem10  30254  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  numclwlk1  30456  frgrregord013  30480  ex-hash  30538  threehalves  32989  evl1deg2  33652  ply1dg3rt0irred  33659  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminplylem5  33946  lmat22det  33982  fib3  34563  prodfzo03  34763  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  aks4d1p1p2  42523  aks4d1p1p7  42527  aks4d1p1  42529  2np3bcnp1  42597  aks6d1c7lem1  42633  3cubeslem3l  43132  3cubeslem3r  43133  jm2.23  43442  resqrtvalex  44090  lt3addmuld  45752  wallispilem4  46514  wallispi2lem1  46517  stirlinglem11  46530  sin3t  47335  sin5tlem4  47340  m1modnep2mod  47818  minusmodnep2tmod  47819  modm1nep2  47834  2timesltsqm1  47839  fmtno0  48015  fmtno5lem4  48031  fmtno4prmfac  48047  fmtno4nprmfac193  48049  139prmALT  48071  31prm  48072  m7prm  48075  lighneallem4a  48083  41prothprmlem2  48093  ppivalnnnprm  48103  2exp340mod341  48221  sbgoldbalt  48269  bgoldbtbndlem1  48293  tgoldbachlt  48304  cycl3grtrilem  48434  gpg5order  48548  gpg3kgrtriexlem2  48572  gpg5gricstgr3  48578  gpgprismgr4cycllem10  48592  pgnbgreunbgrlem2lem2  48603  pgrpgt2nabl  48854  ackval2  49170  ackval3  49171  ackval0012  49177  ackval3012  49180