Theorem 1p2e3 12310

Description: 1 + 2 = 3. For a shorter proof using addcomli 11329, see 1p2e3ALT 12311. (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 12235	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7367	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11146	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12292	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7366	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12309	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2762	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2768	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1547  (class class class)co 7356  1c1 11030   + caddc 11032  2c2 12227  3c3 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addass 11094

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235  df-3 12236

This theorem is referenced by:  fzo1to4tp  13700  binom3  14177  3lcm2e6woprm  16575  prmgaplem7  17019  2exp16  17052  prmlem1a  17068  23prm  17080  prmlem2  17081  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem4  17095  1259prm  17097  2503lem2  17099  2503lem3  17100  4001lem2  17103  quart1lem  26837  log2ublem3  26930  log2ub  26931  pntibndlem2  27572  1kp2ke3k  30534  ex-ind-dvds  30549  cos9thpiminplylem2  33967  fib4  34588  2np3bcnp1  42629  1p3e4  42742  ex-decpmul  42783  sn-0ne2  42883  3cubeslem3r  43136  rabren3dioph  43260  cos3t  47335  modm2nep1  47835  fmtno4nprmfac193  48052  139prmALT  48074  127prm  48077  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  pgnbgreunbgrlem2lem1  48605  gpg5edgnedg  48621  ackval1012  49181