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

Theorem 1p2e3 12297
Description: 1 + 2 = 3. For a shorter proof using addcomli 11348, see 1p2e3ALT 12298. (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 12217 . . 3 2 = (1 + 1)
21oveq2i 7369 . 2 (1 + 2) = (1 + (1 + 1))
3 ax-1cn 11110 . . 3 1 ∈ ℂ
43, 3, 3addassi 11166 . 2 ((1 + 1) + 1) = (1 + (1 + 1))
5 1p1e2 12279 . . . 4 (1 + 1) = 2
65oveq1i 7368 . . 3 ((1 + 1) + 1) = (2 + 1)
7 2p1e3 12296 . . 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 1542  (class class class)co 7358  1c1 11053   + caddc 11055  2c2 12209  3c3 12210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-addass 11117
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-2 12217  df-3 12218
This theorem is referenced by:  fzo1to4tp  13661  binom3  14128  3lcm2e6woprm  16492  prmgaplem7  16930  2exp16  16964  prmlem1a  16980  23prm  16992  prmlem2  16993  83prm  16996  139prm  16997  163prm  16998  317prm  16999  631prm  17000  1259lem4  17007  1259prm  17009  2503lem2  17011  2503lem3  17012  4001lem2  17015  quart1lem  26208  log2ublem3  26301  log2ub  26302  pntibndlem2  26942  1kp2ke3k  29393  ex-ind-dvds  29408  fib4  33007  2np3bcnp1  40555  2xp3dxp2ge1d  40617  ex-decpmul  40809  sn-0ne2  40878  3cubeslem3r  41013  rabren3dioph  41141  fmtno4nprmfac193  45773  139prmALT  45795  127prm  45798  nnsum4primesodd  45995  nnsum4primesoddALTV  45996  ackval1012  46783
  Copyright terms: Public domain W3C validator