Theorem 1p2e3 12319

Description: 1 + 2 = 3. For a shorter proof using addcomli 11338, see 1p2e3ALT 12320. (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 12244	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7378	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11155	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12301	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7377	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12318	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2759	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2765	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  2c2 12236  3c3 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addass 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245

This theorem is referenced by:  fzo1to4tp  13709  binom3  14186  3lcm2e6woprm  16584  prmgaplem7  17028  2exp16  17061  prmlem1a  17077  23prm  17089  prmlem2  17090  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem4  17104  1259prm  17106  2503lem2  17108  2503lem3  17109  4001lem2  17112  quart1lem  26819  log2ublem3  26912  log2ub  26913  pntibndlem2  27554  1kp2ke3k  30516  ex-ind-dvds  30531  cos9thpiminplylem2  33927  fib4  34548  2np3bcnp1  42583  1p3e4  42697  ex-decpmul  42738  sn-0ne2  42838  3cubeslem3r  43119  rabren3dioph  43243  cos3t  47320  modm2nep1  47820  fmtno4nprmfac193  48037  139prmALT  48059  127prm  48062  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  pgnbgreunbgrlem2lem1  48590  gpg5edgnedg  48606  ackval1012  49166