Theorem 2p1e3 12294

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

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  2c2 12212  3c3 12213

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 12221

This theorem is referenced by:  1p2e3  12295  1p2e3ALT  12296  halfthird  12374  halfpm6th  12375  cnm2m1cnm3  12406  6t5e30  12726  7t5e35  12731  8t4e32  12736  9t4e36  12743  decbin3  12761  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  fzo0to42pr  13681  m1modge3gt1  13853  fac3  14215  hash3  14341  hashtplei  14419  hashtpg  14420  hash3tpexb  14429  s3len  14829  repsw3  14886  bpoly3  15993  bpoly4  15994  nn0o1gt2  16320  flodddiv4  16354  ge2nprmge4  16640  3exp3  17031  13prm  17055  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem2  17077  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem4  17083  4001prm  17084  mcubic  26825  log2ublem3  26926  log2ub  26927  birthday  26932  chtub  27191  2lgsoddprmlem3c  27391  istrkg3ld  28545  usgr2wlkspthlem2  29843  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  elwwlks2  30054  elwspths2spth  30055  clwwlknonex2lem1  30194  clwwlknonex2lem2  30195  3wlkdlem5  30250  3wlkdlem10  30256  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  numclwlk1  30458  frgrregord013  30482  ex-hash  30540  threehalves  33007  evl1deg2  33670  ply1dg3rt0irred  33677  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem5  33964  lmat22det  34000  fib3  34581  prodfzo03  34781  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  aks4d1p1p2  42440  aks4d1p1p7  42444  aks4d1p1  42446  2np3bcnp1  42514  aks6d1c7lem1  42550  3cubeslem3l  43043  3cubeslem3r  43044  jm2.23  43353  resqrtvalex  44001  lt3addmuld  45663  wallispilem4  46426  wallispi2lem1  46429  stirlinglem11  46442  m1modnep2mod  47712  minusmodnep2tmod  47713  modm1nep2  47728  fmtno0  47900  fmtno5lem4  47916  fmtno4prmfac  47932  fmtno4nprmfac193  47934  139prmALT  47956  31prm  47957  m7prm  47960  lighneallem4a  47968  41prothprmlem2  47978  2exp340mod341  48093  sbgoldbalt  48141  bgoldbtbndlem1  48165  tgoldbachlt  48176  cycl3grtrilem  48306  gpg5order  48420  gpg3kgrtriexlem2  48444  gpg5gricstgr3  48450  gpgprismgr4cycllem10  48464  pgnbgreunbgrlem2lem2  48475  pgrpgt2nabl  48726  ackval2  49042  ackval3  49043  ackval0012  49049  ackval3012  49052