Theorem 2p1e3 11028

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

Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818  2c2 10947  3c3 10948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-3 10957

This theorem is referenced by:  1p2e3  11029  cnm2m1cnm3  11162  6t5e30  11520  6t5e30OLD  11521  7t5e35  11527  8t4e32  11532  9t4e36  11541  decbin3  11560  halfthird  11561  fz0to3un2pr  12310  m1modge3gt1  12579  fac3  12929  hash3  13055  hashtplei  13120  hashtpg  13121  s3len  13489  repsw3  13542  bpoly3  14628  bpoly4  14629  nn0o1gt2  14935  flodddiv4  14975  3exp3  15636  13prm  15661  37prm  15666  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem2  15683  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem4  15689  4001prm  15690  dcubic1lem  24370  dcubic2  24371  mcubic  24374  log2ublem3  24475  log2ub  24476  birthday  24481  chtub  24737  2lgsoddprmlem3c  24937  istrkg3ld  25160  3v3e3cycl1  26172  constr3trllem5  26182  4cycl4v4e  26194  4cycl4dv4e  26196  extwwlkfablem2  26605  numclwwlkovf2ex  26613  frgraregord013  26645  ex-hash  26702  lmat22det  29216  fib3  29792  jm2.23  36581  lt3addmuld  38456  wallispilem4  38961  wallispi2lem1  38964  stirlinglem11  38977  fmtno0  39990  fmtno5lem4  40006  fmtno4prmfac  40022  fmtno4nprmfac193  40024  139prmALT  40049  31prm  40050  m7prm  40054  lighneallem4a  40063  41prothprmlem2  40073  sgoldbalt  40203  bgoldbtbndlem1  40221  tgoldbachlt  40230  tgoldbachltOLD  40237  usgr2wlkspthlem2  40964  wwlks2onv  41158  elwwlks2ons3  41159  umgrwwlks2on  41161  elwwlks2  41170  elwspths2spth  41171  31wlkdlem5  41330  31wlkdlem10  41336  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  av-numclwwlkovf2ex  41517  av-frgraregord013  41549  pgrpgt2nabl  41941