Theorem 1p2e3 12407

Description: 1 + 2 = 3. For a shorter proof using addcomli 11426, see 1p2e3ALT 12408. (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 12327	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7424	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11182	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11243	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12388	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7423	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12406	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2783	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2789	1 ⊢ (1 + 2) = 3

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7413  1c1 11125   + caddc 11127  2c2 12319  3c3 12320

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 2147  ax-9 2155  ax-ext 2732  ax-1cn 11182  ax-addass 11189

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7416  df-2 12327  df-3 12328

This theorem is used by:  fzo1to4tp  13810  binom3  14288  3lcm2e6woprm  16705  prmgaplem7  17149  2exp16  17182  prmlem1a  17198  23prm  17211  prmlem2  17212  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem4  17226  1259prm  17228  2503lem2  17230  2503lem3  17231  4001lem2  17234  quart1lem  27092  log2ublem3  27185  log2ub  27186  pntibndlem2  27827  1kp2ke3k  30926  ex-ind-dvds  30941  cos9thpiminplylem2  34293  fib4  34915  2np3bcnp1  43010  1p3e4  43126  2p3e5  43132  ex-decpmul  43181  sn-0ne2  43281  3cubeslem3r  43532  rabren3dioph  43656  cos3t  47736  modm2nep1  48260  fmtno4nprmfac193  48477  139prmALT  48499  127prm  48502  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  pgnbgreunbgrlem2lem1  49030  gpg5edgnedg  49046  ackval1012  49620  crosspdotsumlem  50797  crosspaltd  50799  crossp3d  50800