Theorem 1p2e3 12382

Description: 1 + 2 = 3. For a shorter proof using addcomli 11401, see 1p2e3ALT 12383. (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 12302	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7422	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11157	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11218	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12363	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7421	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12381	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2792	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2798	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11100   + caddc 11102  2c2 12294  3c3 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-addass 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302  df-3 12303

This theorem is referenced by:  fzo1to4tp  13782  binom3  14259  3lcm2e6woprm  16672  prmgaplem7  17116  2exp16  17149  prmlem1a  17165  23prm  17178  prmlem2  17179  83prm  17182  139prm  17183  163prm  17184  317prm  17185  631prm  17186  1259lem4  17193  1259prm  17195  2503lem2  17197  2503lem3  17198  4001lem2  17201  quart1lem  26985  log2ublem3  27078  log2ub  27079  pntibndlem2  27720  1kp2ke3k  30737  ex-ind-dvds  30752  cos9thpiminplylem2  34117  fib4  34738  2np3bcnp1  42800  1p3e4  42915  ex-decpmul  42956  sn-0ne2  43056  3cubeslem3r  43309  rabren3dioph  43433  cos3t  47497  modm2nep1  47997  fmtno4nprmfac193  48214  139prmALT  48236  127prm  48239  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  pgnbgreunbgrlem2lem1  48767  gpg5edgnedg  48783  ackval1012  49354