Theorem 1p2e3 12283

Description: 1 + 2 = 3. For a shorter proof using addcomli 11325, see 1p2e3ALT 12284. (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 12208	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7369	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11142	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12265	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7368	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12282	. . 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 1541  (class class class)co 7358  1c1 11027   + caddc 11029  2c2 12200  3c3 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addass 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208  df-3 12209

This theorem is referenced by:  fzo1to4tp  13670  binom3  14147  3lcm2e6woprm  16542  prmgaplem7  16985  2exp16  17018  prmlem1a  17034  23prm  17046  prmlem2  17047  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem4  17061  1259prm  17063  2503lem2  17065  2503lem3  17066  4001lem2  17069  quart1lem  26821  log2ublem3  26914  log2ub  26915  pntibndlem2  27558  1kp2ke3k  30521  ex-ind-dvds  30536  cos9thpiminplylem2  33940  fib4  34561  2np3bcnp1  42398  1p3e4  42514  ex-decpmul  42561  sn-0ne2  42661  3cubeslem3r  42929  rabren3dioph  43057  modm2nep1  47612  fmtno4nprmfac193  47820  139prmALT  47842  127prm  47845  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  pgnbgreunbgrlem2lem1  48360  gpg5edgnedg  48376  ackval1012  48936