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 2748	1 ⊢ (2 + 1) = 3

Syntax hints:   = wceq 1547  (class class class)co 7356  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  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  26829  log2ublem3  26930  log2ub  26931  birthday  26936  chtub  27193  2lgsoddprmlem3c  27393  istrkg3ld  28547  usgr2wlkspthlem2  29844  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  elwwlks2  30055  elwspths2spth  30056  clwwlknonex2lem1  30195  clwwlknonex2lem2  30196  3wlkdlem5  30251  3wlkdlem10  30257  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  numclwlk1  30459  frgrregord013  30483  ex-hash  30541  threehalves  32993  evl1deg2  33660  ply1dg3rt0irred  33667  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem5  33970  lmat22det  34006  fib3  34587  prodfzo03  34787  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  aks4d1p1p2  42555  aks4d1p1p7  42559  aks4d1p1  42561  2np3bcnp1  42629  aks6d1c7lem1  42665  3cubeslem3l  43135  3cubeslem3r  43136  jm2.23  43441  resqrtvalex  44089  lt3addmuld  45749  wallispilem4  46511  wallispi2lem1  46514  stirlinglem11  46527  sin3t  47334  sin5tlem4  47339  m1modnep2mod  47821  minusmodnep2tmod  47822  modm1nep2  47837  2timesltsqm1  47842  fmtno0  48018  fmtno5lem4  48034  fmtno4prmfac  48050  fmtno4nprmfac193  48052  139prmALT  48074  31prm  48075  m7prm  48078  lighneallem4a  48086  41prothprmlem2  48096  ppivalnnnprm  48106  2exp340mod341  48224  sbgoldbalt  48272  bgoldbtbndlem1  48296  tgoldbachlt  48307  cycl3grtrilem  48437  gpg5order  48551  gpg3kgrtriexlem2  48575  gpg5gricstgr3  48581  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem2lem2  48606  pgrpgt2nabl  48857  ackval2  49173  ackval3  49174  ackval0012  49180  ackval3012  49183