MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1p2e3 Structured version   Visualization version   GIF version

Theorem 1p2e3 11777
Description: 1 + 2 = 3. For a shorter proof using addcomli 10830, see 1p2e3ALT 11778. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 12-Dec-2022.)
Assertion
Ref Expression
1p2e3 (1 + 2) = 3

Proof of Theorem 1p2e3
StepHypRef Expression
1 df-2 11697 . . 3 2 = (1 + 1)
21oveq2i 7160 . 2 (1 + 2) = (1 + (1 + 1))
3 ax-1cn 10593 . . 3 1 ∈ ℂ
43, 3, 3addassi 10649 . 2 ((1 + 1) + 1) = (1 + (1 + 1))
5 1p1e2 11759 . . . 4 (1 + 1) = 2
65oveq1i 7159 . . 3 ((1 + 1) + 1) = (2 + 1)
7 2p1e3 11776 . . 3 (2 + 1) = 3
86, 7eqtri 2847 . 2 ((1 + 1) + 1) = 3
92, 4, 83eqtr2i 2853 1 (1 + 2) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7149  1c1 10536   + caddc 10538  2c2 11689  3c3 11690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10593  ax-addass 10600
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152  df-2 11697  df-3 11698
This theorem is referenced by:  fzo1to4tp  13129  binom3  13590  3lcm2e6woprm  15957  prmgaplem7  16391  2exp16  16424  prmlem1a  16440  23prm  16452  prmlem2  16453  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem4  16467  1259prm  16469  2503lem2  16471  2503lem3  16472  4001lem2  16475  quart1lem  25444  log2ublem3  25537  log2ub  25538  pntibndlem2  26178  1kp2ke3k  28234  ex-ind-dvds  28249  fib4  31719  2np3bcnp1  39294  2xp3dxp2ge1d  39324  ex-decpmul  39416  sn-0ne2  39474  3cubeslem3r  39544  rabren3dioph  39672  fmtno4nprmfac193  44017  139prmALT  44039  127prm  44042  nnsum4primesodd  44240  nnsum4primesoddALTV  44241  ackval1012  45030
  Copyright terms: Public domain W3C validator