Theorem 1p2e3 12378

Description: 1 + 2 = 3. For a shorter proof using addcomli 11397, see 1p2e3ALT 12379. (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

Step	Hyp	Ref	Expression
1		df-2 12298	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7421	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11214	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12359	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7420	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12377	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2786	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2792	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   + caddc 11098  2c2 12290  3c3 12291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addass 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299

This theorem is referenced by:  fzo1to4tp  13779  binom3  14256  3lcm2e6woprm  16668  prmgaplem7  17112  2exp16  17145  prmlem1a  17161  23prm  17174  prmlem2  17175  83prm  17178  139prm  17179  163prm  17180  317prm  17181  631prm  17182  1259lem4  17189  1259prm  17191  2503lem2  17193  2503lem3  17194  4001lem2  17197  quart1lem  27020  log2ublem3  27113  log2ub  27114  pntibndlem2  27755  1kp2ke3k  30797  ex-ind-dvds  30812  cos9thpiminplylem2  34173  fib4  34794  2np3bcnp1  42911  1p3e4  43026  ex-decpmul  43067  sn-0ne2  43167  3cubeslem3r  43418  rabren3dioph  43542  cos3t  47609  modm2nep1  48109  fmtno4nprmfac193  48326  139prmALT  48348  127prm  48351  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  pgnbgreunbgrlem2lem1  48879  gpg5edgnedg  48895  ackval1012  49470