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

Theorem 1p2e3 12409
Description: 1 + 2 = 3. For a shorter proof using addcomli 11453, see 1p2e3ALT 12410. (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 12329 . . 3 2 = (1 + 1)
21oveq2i 7442 . 2 (1 + 2) = (1 + (1 + 1))
3 ax-1cn 11213 . . 3 1 ∈ ℂ
43, 3, 3addassi 11271 . 2 ((1 + 1) + 1) = (1 + (1 + 1))
5 1p1e2 12391 . . . 4 (1 + 1) = 2
65oveq1i 7441 . . 3 ((1 + 1) + 1) = (2 + 1)
7 2p1e3 12408 . . 3 (2 + 1) = 3
86, 7eqtri 2765 . 2 ((1 + 1) + 1) = 3
92, 4, 83eqtr2i 2771 1 (1 + 2) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  2c2 12321  3c3 12322
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addass 11220
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330
This theorem is referenced by:  fzo1to4tp  13793  binom3  14263  3lcm2e6woprm  16652  prmgaplem7  17095  2exp16  17128  prmlem1a  17144  23prm  17156  prmlem2  17157  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem4  17171  1259prm  17173  2503lem2  17175  2503lem3  17176  4001lem2  17179  quart1lem  26898  log2ublem3  26991  log2ub  26992  pntibndlem2  27635  1kp2ke3k  30465  ex-ind-dvds  30480  fib4  34406  2np3bcnp1  42145  2xp3dxp2ge1d  42242  ex-decpmul  42340  sn-0ne2  42436  3cubeslem3r  42698  rabren3dioph  42826  fmtno4nprmfac193  47561  139prmALT  47583  127prm  47586  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  ackval1012  48611
  Copyright terms: Public domain W3C validator