Theorem 2p1e3 12318

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  2c2 12236  3c3 12237

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 2708

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

This theorem is referenced by:  1p2e3  12319  1p2e3ALT  12320  halfthird  12398  halfpm6th  12399  cnm2m1cnm3  12430  6t5e30  12751  7t5e35  12756  8t4e32  12761  9t4e36  12768  decbin3  12786  fz0to3un2pr  13583  fz0to4untppr  13584  fz0to5un2tp  13585  fzo0to42pr  13708  m1modge3gt1  13880  fac3  14242  hash3  14368  hashtplei  14446  hashtpg  14447  hash3tpexb  14456  s3len  14856  repsw3  14913  bpoly3  16023  bpoly4  16024  nn0o1gt2  16350  flodddiv4  16384  ge2nprmge4  16671  3exp3  17062  13prm  17086  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem2  17108  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  mcubic  26811  log2ublem3  26912  log2ub  26913  birthday  26918  chtub  27175  2lgsoddprmlem3c  27375  istrkg3ld  28529  usgr2wlkspthlem2  29826  elwwlks2ons3im  30022  usgrwwlks2on  30026  umgrwwlks2on  30027  elwwlks2  30037  elwspths2spth  30038  clwwlknonex2lem1  30177  clwwlknonex2lem2  30178  3wlkdlem5  30233  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  numclwlk1  30441  frgrregord013  30465  ex-hash  30523  threehalves  32974  evl1deg2  33637  ply1dg3rt0irred  33644  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem5  33930  lmat22det  33966  fib3  34547  prodfzo03  34747  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  aks4d1p1p2  42509  aks4d1p1p7  42513  aks4d1p1  42515  2np3bcnp1  42583  aks6d1c7lem1  42619  3cubeslem3l  43118  3cubeslem3r  43119  jm2.23  43424  resqrtvalex  44072  lt3addmuld  45734  wallispilem4  46496  wallispi2lem1  46499  stirlinglem11  46512  sin3t  47319  sin5tlem4  47324  m1modnep2mod  47806  minusmodnep2tmod  47807  modm1nep2  47822  2timesltsqm1  47827  fmtno0  48003  fmtno5lem4  48019  fmtno4prmfac  48035  fmtno4nprmfac193  48037  139prmALT  48059  31prm  48060  m7prm  48063  lighneallem4a  48071  41prothprmlem2  48081  ppivalnnnprm  48091  2exp340mod341  48209  sbgoldbalt  48257  bgoldbtbndlem1  48281  tgoldbachlt  48292  cycl3grtrilem  48422  gpg5order  48536  gpg3kgrtriexlem2  48560  gpg5gricstgr3  48566  gpgprismgr4cycllem10  48580  pgnbgreunbgrlem2lem2  48591  pgrpgt2nabl  48842  ackval2  49158  ackval3  49159  ackval0012  49165  ackval3012  49168