Theorem 1p2e3 12331

Description: 1 + 2 = 3. For a shorter proof using addcomli 11373, see 1p2e3ALT 12332. (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 12256	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7401	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11191	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12313	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7400	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12330	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2753	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2759	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  2c2 12248  3c3 12249

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-addass 11140

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257

This theorem is referenced by:  fzo1to4tp  13722  binom3  14196  3lcm2e6woprm  16592  prmgaplem7  17035  2exp16  17068  prmlem1a  17084  23prm  17096  prmlem2  17097  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem4  17111  1259prm  17113  2503lem2  17115  2503lem3  17116  4001lem2  17119  quart1lem  26772  log2ublem3  26865  log2ub  26866  pntibndlem2  27509  1kp2ke3k  30382  ex-ind-dvds  30397  cos9thpiminplylem2  33780  fib4  34402  2np3bcnp1  42139  1p3e4  42254  ex-decpmul  42301  sn-0ne2  42401  3cubeslem3r  42682  rabren3dioph  42810  modm2nep1  47371  fmtno4nprmfac193  47579  139prmALT  47601  127prm  47604  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  pgnbgreunbgrlem2lem1  48108  ackval1012  48683