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

Theorem 1p2e3 12002
Description: 1 + 2 = 3. For a shorter proof using addcomli 11053, see 1p2e3ALT 12003. (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 11922 . . 3 2 = (1 + 1)
21oveq2i 7245 . 2 (1 + 2) = (1 + (1 + 1))
3 ax-1cn 10816 . . 3 1 ∈ ℂ
43, 3, 3addassi 10872 . 2 ((1 + 1) + 1) = (1 + (1 + 1))
5 1p1e2 11984 . . . 4 (1 + 1) = 2
65oveq1i 7244 . . 3 ((1 + 1) + 1) = (2 + 1)
7 2p1e3 12001 . . 3 (2 + 1) = 3
86, 7eqtri 2767 . 2 ((1 + 1) + 1) = 3
92, 4, 83eqtr2i 2773 1 (1 + 2) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  (class class class)co 7234  1c1 10759   + caddc 10761  2c2 11914  3c3 11915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710  ax-1cn 10816  ax-addass 10823
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-iota 6358  df-fv 6408  df-ov 7237  df-2 11922  df-3 11923
This theorem is referenced by:  fzo1to4tp  13359  binom3  13823  3lcm2e6woprm  16204  prmgaplem7  16642  2exp16  16676  prmlem1a  16692  23prm  16704  prmlem2  16705  83prm  16708  139prm  16709  163prm  16710  317prm  16711  631prm  16712  1259lem4  16719  1259prm  16721  2503lem2  16723  2503lem3  16724  4001lem2  16727  quart1lem  25769  log2ublem3  25862  log2ub  25863  pntibndlem2  26503  1kp2ke3k  28560  ex-ind-dvds  28575  fib4  32114  2np3bcnp1  39863  2xp3dxp2ge1d  39925  ex-decpmul  40075  sn-0ne2  40144  3cubeslem3r  40259  rabren3dioph  40387  fmtno4nprmfac193  44744  139prmALT  44766  127prm  44769  nnsum4primesodd  44966  nnsum4primesoddALTV  44967  ackval1012  45754
  Copyright terms: Public domain W3C validator