Theorem 1p2e3 12360

Description: 1 + 2 = 3. For a shorter proof using addcomli 11375, see 1p2e3ALT 12361. (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 12280	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7407	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11192	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12341	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7406	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12359	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2785	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2791	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1560  (class class class)co 7396  1c1 11074   + caddc 11076  2c2 12272  3c3 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addass 11138

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281

This theorem is referenced by:  fzo1to4tp  13760  binom3  14237  3lcm2e6woprm  16649  prmgaplem7  17093  2exp16  17126  prmlem1a  17142  23prm  17155  prmlem2  17156  83prm  17159  139prm  17160  163prm  17161  317prm  17162  631prm  17163  1259lem4  17170  1259prm  17172  2503lem2  17174  2503lem3  17175  4001lem2  17178  quart1lem  26917  log2ublem3  27010  log2ub  27011  pntibndlem2  27652  1kp2ke3k  30645  ex-ind-dvds  30660  cos9thpiminplylem2  34077  fib4  34698  2np3bcnp1  42758  1p3e4  42871  ex-decpmul  42912  sn-0ne2  43012  3cubeslem3r  43265  rabren3dioph  43389  cos3t  47463  modm2nep1  47963  fmtno4nprmfac193  48180  139prmALT  48202  127prm  48205  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  pgnbgreunbgrlem2lem1  48733  gpg5edgnedg  48749  ackval1012  49309