Theorem 2p1e3 12299

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  2c2 12217  3c3 12218

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  1p2e3  12300  1p2e3ALT  12301  halfthird  12379  halfpm6th  12380  cnm2m1cnm3  12411  6t5e30  12732  7t5e35  12737  8t4e32  12742  9t4e36  12749  decbin3  12767  fz0to3un2pr  13566  fz0to4untppr  13567  fz0to5un2tp  13568  fzo0to42pr  13690  m1modge3gt1  13859  fac3  14221  hash3  14347  hashtplei  14425  hashtpg  14426  hash3tpexb  14435  s3len  14836  repsw3  14893  bpoly3  16000  bpoly4  16001  nn0o1gt2  16327  flodddiv4  16361  ge2nprmge4  16647  3exp3  17038  13prm  17062  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem2  17084  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem4  17090  4001prm  17091  mcubic  26733  log2ublem3  26834  log2ub  26835  birthday  26840  chtub  27099  2lgsoddprmlem3c  27299  istrkg3ld  28364  usgr2wlkspthlem2  29661  elwwlks2ons3im  29857  umgrwwlks2on  29860  elwwlks2  29869  elwspths2spth  29870  clwwlknonex2lem1  30009  clwwlknonex2lem2  30010  3wlkdlem5  30065  3wlkdlem10  30071  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  numclwlk1  30273  frgrregord013  30297  ex-hash  30355  threehalves  32808  evl1deg2  33519  ply1dg3rt0irred  33524  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem5  33749  lmat22det  33785  fib3  34367  prodfzo03  34567  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  aks4d1p1p2  42031  aks4d1p1p7  42035  aks4d1p1  42037  2np3bcnp1  42105  aks6d1c7lem1  42141  3cubeslem3l  42647  3cubeslem3r  42648  jm2.23  42958  resqrtvalex  43607  lt3addmuld  45272  wallispilem4  46039  wallispi2lem1  46042  stirlinglem11  46055  m1modnep2mod  47326  minusmodnep2tmod  47327  modm1nep2  47342  fmtno0  47514  fmtno5lem4  47530  fmtno4prmfac  47546  fmtno4nprmfac193  47548  139prmALT  47570  31prm  47571  m7prm  47574  lighneallem4a  47582  41prothprmlem2  47592  2exp340mod341  47707  sbgoldbalt  47755  bgoldbtbndlem1  47779  tgoldbachlt  47790  cycl3grtrilem  47918  gpg5order  48024  gpg3kgrtriexlem2  48048  gpg5gricstgr3  48054  gpgprismgr4cycllem10  48067  pgnbgreunbgrlem2lem2  48078  pgrpgt2nabl  48327  ackval2  48644  ackval3  48645  ackval0012  48651  ackval3012  48654