Theorem 2p1e3 12405

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

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   + caddc 11155  2c2 12318  3c3 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-3 12327

This theorem is referenced by:  1p2e3  12406  1p2e3ALT  12407  cnm2m1cnm3  12516  6t5e30  12837  7t5e35  12842  8t4e32  12847  9t4e36  12854  decbin3  12872  halfthird  12873  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  fzo0to42pr  13788  m1modge3gt1  13955  fac3  14315  hash3  14441  hashtplei  14519  hashtpg  14520  hash3tpexb  14529  s3len  14929  repsw3  14986  bpoly3  16090  bpoly4  16091  nn0o1gt2  16414  flodddiv4  16448  ge2nprmge4  16734  3exp3  17125  13prm  17149  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem2  17171  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem4  17177  4001prm  17178  mcubic  26904  log2ublem3  27005  log2ub  27006  birthday  27011  chtub  27270  2lgsoddprmlem3c  27470  istrkg3ld  28483  usgr2wlkspthlem2  29790  elwwlks2ons3im  29983  umgrwwlks2on  29986  elwwlks2  29995  elwspths2spth  29996  clwwlknonex2lem1  30135  clwwlknonex2lem2  30136  3wlkdlem5  30191  3wlkdlem10  30197  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  numclwlk1  30399  frgrregord013  30423  ex-hash  30481  threehalves  32881  evl1deg2  33581  ply1dg3rt0irred  33586  lmat22det  33782  fib3  34384  prodfzo03  34596  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  aks4d1p1p2  42051  aks4d1p1p7  42055  aks4d1p1  42057  2np3bcnp1  42125  aks6d1c7lem1  42161  3cubeslem3l  42673  3cubeslem3r  42674  jm2.23  42984  resqrtvalex  43634  lt3addmuld  45251  wallispilem4  46023  wallispi2lem1  46026  stirlinglem11  46039  m1modnep2mod  47291  minusmodnep2tmod  47292  fmtno0  47464  fmtno5lem4  47480  fmtno4prmfac  47496  fmtno4nprmfac193  47498  139prmALT  47520  31prm  47521  m7prm  47524  lighneallem4a  47532  41prothprmlem2  47542  2exp340mod341  47657  sbgoldbalt  47705  bgoldbtbndlem1  47729  tgoldbachlt  47740  gpg5order  47948  gpg5gricstgr3  47973  pgrpgt2nabl  48210  ackval2  48531  ackval3  48532  ackval0012  48538  ackval3012  48541