Theorem 1p2e3 12295

Description: 1 + 2 = 3. For a shorter proof using addcomli 11337, see 1p2e3ALT 12296. (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 12220	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7379	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11154	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12277	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7378	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12294	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2760	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2766	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  2c2 12212  3c3 12213

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221

This theorem is referenced by:  fzo1to4tp  13682  binom3  14159  3lcm2e6woprm  16554  prmgaplem7  16997  2exp16  17030  prmlem1a  17046  23prm  17058  prmlem2  17059  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem4  17073  1259prm  17075  2503lem2  17077  2503lem3  17078  4001lem2  17081  quart1lem  26833  log2ublem3  26926  log2ub  26927  pntibndlem2  27570  1kp2ke3k  30533  ex-ind-dvds  30548  cos9thpiminplylem2  33961  fib4  34582  2np3bcnp1  42514  1p3e4  42629  ex-decpmul  42676  sn-0ne2  42776  3cubeslem3r  43044  rabren3dioph  43172  modm2nep1  47726  fmtno4nprmfac193  47934  139prmALT  47956  127prm  47959  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  pgnbgreunbgrlem2lem1  48474  gpg5edgnedg  48490  ackval1012  49050