Theorem 2p1e3 12378

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

Syntax hints:   = wceq 1567  (class class class)co 7408  1c1 11097   + caddc 11099  2c2 12291  3c3 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-3 12300

This theorem is referenced by:  1p2e3  12379  1p2e3ALT  12380  halfthird  12461  halfpm6th  12462  cnm2m1cnm3  12493  6t5e30  12819  7t5e35  12824  8t4e32  12829  9t4e36  12836  decbin3  12856  fz0to3un2pr  13653  fz0to4untppr  13654  fz0to5un2tp  13655  fzo0to42pr  13778  m1modge3gt1  13950  fac3  14312  hash3  14438  hashtplei  14517  hashtpg  14518  hash3tpexb  14527  s3len  14927  repsw3  14984  bpoly3  16108  bpoly4  16109  nn0o1gt2  16435  flodddiv4  16469  ge2nprmge4  16756  3exp3  17147  13prm  17172  37prm  17177  43prm  17178  83prm  17179  139prm  17180  163prm  17181  317prm  17182  631prm  17183  1259lem1  17187  1259lem2  17188  1259lem3  17189  1259lem4  17190  1259lem5  17191  1259prm  17192  2503lem2  17194  2503prm  17196  4001lem1  17197  4001lem2  17198  4001lem4  17200  4001prm  17201  mcubic  26974  log2ublem3  27075  log2ub  27076  birthday  27081  chtub  27338  2lgsoddprmlem3c  27538  istrkg3ld  28692  usgr2wlkspthlem2  30044  elwwlks2ons3im  30240  usgrwwlks2on  30244  umgrwwlks2on  30245  elwwlks2  30255  elwspths2spth  30256  clwwlknonex2lem1  30395  clwwlknonex2lem2  30396  3wlkdlem5  30451  3wlkdlem10  30457  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  numclwlk1  30659  frgrregord013  30683  ex-hash  30741  threehalves  33171  evl1deg2  33808  ply1dg3rt0irred  33815  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminplylem5  34117  lmat22det  34153  fib3  34734  prodfzo03  34931  hgt750lemd  34976  hgt750lem  34979  hgt750lem2  34980  aks4d1p1p2  42722  aks4d1p1p7  42726  aks4d1p1  42728  2np3bcnp1  42796  aks6d1c7lem1  42832  3cubeslem3l  43304  3cubeslem3r  43305  jm2.23  43610  resqrtvalex  44258  lt3addmuld  45907  wallispilem4  46669  wallispi2lem1  46672  stirlinglem11  46685  sin3t  47492  sin5tlem4  47497  m1modnep2mod  47979  minusmodnep2tmod  47980  modm1nep2  47995  2timesltsqm1  48000  fmtno0  48176  fmtno5lem4  48192  fmtno4prmfac  48208  fmtno4nprmfac193  48210  139prmALT  48232  31prm  48233  m7prm  48236  lighneallem4a  48244  41prothprmlem2  48254  ppivalnnnprm  48264  2exp340mod341  48382  sbgoldbalt  48430  bgoldbtbndlem1  48454  tgoldbachlt  48465  cycl3grtrilem  48595  gpg5order  48709  gpg3kgrtriexlem2  48733  gpg5gricstgr3  48739  gpgprismgr4cycllem10  48753  pgnbgreunbgrlem2lem2  48764  pgrpgt2nabl  49026  ackval2  49342  ackval3  49343  ackval0012  49349  ackval3012  49352