Theorem 2p1e3 12265

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  2c2 12183  3c3 12184

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 12192

This theorem is referenced by:  1p2e3  12266  1p2e3ALT  12267  halfthird  12345  halfpm6th  12346  cnm2m1cnm3  12377  6t5e30  12698  7t5e35  12703  8t4e32  12708  9t4e36  12715  decbin3  12733  fz0to3un2pr  13532  fz0to4untppr  13533  fz0to5un2tp  13534  fzo0to42pr  13656  m1modge3gt1  13825  fac3  14187  hash3  14313  hashtplei  14391  hashtpg  14392  hash3tpexb  14401  s3len  14801  repsw3  14858  bpoly3  15965  bpoly4  15966  nn0o1gt2  16292  flodddiv4  16326  ge2nprmge4  16612  3exp3  17003  13prm  17027  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem2  17049  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem4  17055  4001prm  17056  mcubic  26755  log2ublem3  26856  log2ub  26857  birthday  26862  chtub  27121  2lgsoddprmlem3c  27321  istrkg3ld  28406  usgr2wlkspthlem2  29703  elwwlks2ons3im  29899  umgrwwlks2on  29902  elwwlks2  29911  elwspths2spth  29912  clwwlknonex2lem1  30051  clwwlknonex2lem2  30052  3wlkdlem5  30107  3wlkdlem10  30113  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  konigsberglem1  30196  konigsberglem2  30197  konigsberglem3  30198  numclwlk1  30315  frgrregord013  30339  ex-hash  30397  threehalves  32855  evl1deg2  33512  ply1dg3rt0irred  33518  cos9thpiminplylem1  33749  cos9thpiminplylem2  33750  cos9thpiminplylem5  33753  lmat22det  33789  fib3  34371  prodfzo03  34571  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  aks4d1p1p2  42043  aks4d1p1p7  42047  aks4d1p1  42049  2np3bcnp1  42117  aks6d1c7lem1  42153  3cubeslem3l  42659  3cubeslem3r  42660  jm2.23  42969  resqrtvalex  43618  lt3addmuld  45283  wallispilem4  46049  wallispi2lem1  46052  stirlinglem11  46065  m1modnep2mod  47336  minusmodnep2tmod  47337  modm1nep2  47352  fmtno0  47524  fmtno5lem4  47540  fmtno4prmfac  47556  fmtno4nprmfac193  47558  139prmALT  47580  31prm  47581  m7prm  47584  lighneallem4a  47592  41prothprmlem2  47602  2exp340mod341  47717  sbgoldbalt  47765  bgoldbtbndlem1  47789  tgoldbachlt  47800  cycl3grtrilem  47930  gpg5order  48044  gpg3kgrtriexlem2  48068  gpg5gricstgr3  48074  gpgprismgr4cycllem10  48088  pgnbgreunbgrlem2lem2  48099  pgrpgt2nabl  48350  ackval2  48667  ackval3  48668  ackval0012  48674  ackval3012  48677