Theorem 1p2e3 12313

Description: 1 + 2 = 3. For a shorter proof using addcomli 11332, see 1p2e3ALT 12314. (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 12238	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7372	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11149	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12295	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7371	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12312	. . 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 7361  1c1 11033   + caddc 11035  2c2 12230  3c3 12231

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 11090  ax-addass 11097

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239

This theorem is referenced by:  fzo1to4tp  13703  binom3  14180  3lcm2e6woprm  16578  prmgaplem7  17022  2exp16  17055  prmlem1a  17071  23prm  17083  prmlem2  17084  83prm  17087  139prm  17088  163prm  17089  317prm  17090  631prm  17091  1259lem4  17098  1259prm  17100  2503lem2  17102  2503lem3  17103  4001lem2  17106  quart1lem  26835  log2ublem3  26928  log2ub  26929  pntibndlem2  27571  1kp2ke3k  30534  ex-ind-dvds  30549  cos9thpiminplylem2  33946  fib4  34567  2np3bcnp1  42600  1p3e4  42714  ex-decpmul  42755  sn-0ne2  42855  3cubeslem3r  43136  rabren3dioph  43264  cos3t  47339  modm2nep1  47835  fmtno4nprmfac193  48052  139prmALT  48074  127prm  48077  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  pgnbgreunbgrlem2lem1  48605  gpg5edgnedg  48621  ackval1012  49181