Theorem 2p1e3 12380

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

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  2c2 12293  3c3 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-3 12302

This theorem is referenced by:  1p2e3  12381  1p2e3ALT  12382  halfthird  12460  halfpm6th  12461  cnm2m1cnm3  12492  6t5e30  12813  7t5e35  12818  8t4e32  12823  9t4e36  12830  decbin3  12848  fz0to3un2pr  13644  fz0to4untppr  13645  fz0to5un2tp  13646  fzo0to42pr  13767  m1modge3gt1  13934  fac3  14296  hash3  14422  hashtplei  14500  hashtpg  14501  hash3tpexb  14510  s3len  14911  repsw3  14968  bpoly3  16072  bpoly4  16073  nn0o1gt2  16398  flodddiv4  16432  ge2nprmge4  16718  3exp3  17109  13prm  17133  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem2  17155  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem4  17161  4001prm  17162  mcubic  26807  log2ublem3  26908  log2ub  26909  birthday  26914  chtub  27173  2lgsoddprmlem3c  27373  istrkg3ld  28386  usgr2wlkspthlem2  29686  elwwlks2ons3im  29882  umgrwwlks2on  29885  elwwlks2  29894  elwspths2spth  29895  clwwlknonex2lem1  30034  clwwlknonex2lem2  30035  3wlkdlem5  30090  3wlkdlem10  30096  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  numclwlk1  30298  frgrregord013  30322  ex-hash  30380  threehalves  32835  evl1deg2  33536  ply1dg3rt0irred  33541  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  cos9thpiminplylem5  33766  lmat22det  33799  fib3  34381  prodfzo03  34581  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  aks4d1p1p2  42029  aks4d1p1p7  42033  aks4d1p1  42035  2np3bcnp1  42103  aks6d1c7lem1  42139  3cubeslem3l  42656  3cubeslem3r  42657  jm2.23  42967  resqrtvalex  43616  lt3addmuld  45278  wallispilem4  46045  wallispi2lem1  46048  stirlinglem11  46061  m1modnep2mod  47329  minusmodnep2tmod  47330  fmtno0  47502  fmtno5lem4  47518  fmtno4prmfac  47534  fmtno4nprmfac193  47536  139prmALT  47558  31prm  47559  m7prm  47562  lighneallem4a  47570  41prothprmlem2  47580  2exp340mod341  47695  sbgoldbalt  47743  bgoldbtbndlem1  47767  tgoldbachlt  47778  cycl3grtrilem  47906  gpg5order  48012  gpg3kgrtriexlem2  48034  gpg5gricstgr3  48040  gpgprismgr4cycllem10  48051  pgrpgt2nabl  48289  ackval2  48610  ackval3  48611  ackval0012  48617  ackval3012  48620