Theorem 1p2e3 12398

Description: 1 + 2 = 3. For a shorter proof using addcomli 11417, see 1p2e3ALT 12399. (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 12318	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7430	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11173	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11234	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12379	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7429	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12397	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2788	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2794	1 ⊢ (1 + 2) = 3

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11116   + caddc 11118  2c2 12310  3c3 12311

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-addass 11180

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12318  df-3 12319

This theorem is used by:  fzo1to4tp  13800  binom3  14278  3lcm2e6woprm  16695  prmgaplem7  17139  2exp16  17172  prmlem1a  17188  23prm  17201  prmlem2  17202  83prm  17205  139prm  17206  163prm  17207  317prm  17208  631prm  17209  1259lem4  17216  1259prm  17218  2503lem2  17220  2503lem3  17221  4001lem2  17224  quart1lem  27071  log2ublem3  27164  log2ub  27165  pntibndlem2  27806  1kp2ke3k  30868  ex-ind-dvds  30883  cos9thpiminplylem2  34237  fib4  34859  2np3bcnp1  42969  1p3e4  43084  ex-decpmul  43125  sn-0ne2  43225  3cubeslem3r  43476  rabren3dioph  43600  cos3t  47667  modm2nep1  48167  fmtno4nprmfac193  48384  139prmALT  48406  127prm  48409  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  pgnbgreunbgrlem2lem1  48937  gpg5edgnedg  48953  ackval1012  49527  crosspdotsumlem  50703  crosspaltd  50705  crossp3d  50706