Theorem 1p2e3 12381

Description: 1 + 2 = 3. For a shorter proof using addcomli 11425, see 1p2e3ALT 12382. (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 12301	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7414	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11243	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12363	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7413	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12380	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2758	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2764	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  2c2 12293  3c3 12294

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addass 11192

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-2 12301  df-3 12302

This theorem is referenced by:  fzo1to4tp  13768  binom3  14240  3lcm2e6woprm  16632  prmgaplem7  17075  2exp16  17108  prmlem1a  17124  23prm  17136  prmlem2  17137  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem4  17151  1259prm  17153  2503lem2  17155  2503lem3  17156  4001lem2  17159  quart1lem  26815  log2ublem3  26908  log2ub  26909  pntibndlem2  27552  1kp2ke3k  30373  ex-ind-dvds  30388  cos9thpiminplylem2  33763  fib4  34382  2np3bcnp1  42103  2xp3dxp2ge1d  42200  ex-decpmul  42302  sn-0ne2  42396  3cubeslem3r  42657  rabren3dioph  42785  fmtno4nprmfac193  47536  139prmALT  47558  127prm  47561  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  ackval1012  48618