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

Theorem 1p2e3 11768
Description: 1 + 2 = 3. For a shorter proof using addcomli 10820, see 1p2e3ALT 11769. (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 11688 . . 3 2 = (1 + 1)
21oveq2i 7156 . 2 (1 + 2) = (1 + (1 + 1))
3 ax-1cn 10583 . . 3 1 ∈ ℂ
43, 3, 3addassi 10639 . 2 ((1 + 1) + 1) = (1 + (1 + 1))
5 1p1e2 11750 . . . 4 (1 + 1) = 2
65oveq1i 7155 . . 3 ((1 + 1) + 1) = (2 + 1)
7 2p1e3 11767 . . 3 (2 + 1) = 3
86, 7eqtri 2841 . 2 ((1 + 1) + 1) = 3
92, 4, 83eqtr2i 2847 1 (1 + 2) = 3
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  1c1 10526   + caddc 10528  2c2 11680  3c3 11681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-1cn 10583  ax-addass 10590
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-2 11688  df-3 11689
This theorem is referenced by:  fzo1to4tp  13113  binom3  13573  3lcm2e6woprm  15947  prmgaplem7  16381  2exp16  16412  prmlem1a  16428  23prm  16440  prmlem2  16441  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem4  16455  1259prm  16457  2503lem2  16459  2503lem3  16460  4001lem2  16463  quart1lem  25360  log2ublem3  25453  log2ub  25454  pntibndlem2  26094  1kp2ke3k  28152  ex-ind-dvds  28167  fib4  31561  ex-decpmul  39056  sn-0ne2  39114  3cubeslem3r  39162  rabren3dioph  39290  fmtno4nprmfac193  43613  139prmALT  43636  127prm  43640  nnsum4primesodd  43838  nnsum4primesoddALTV  43839
  Copyright terms: Public domain W3C validator