Theorem 1p2e3 11525

Description: 1 + 2 = 3. For a shorter proof using addcomli 10568, see 1p2e3ALT 11526. (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 11438	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 6933	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 10330	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 10387	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 11507	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 6932	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 11524	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2802	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2808	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1601  (class class class)co 6922  1c1 10273   + caddc 10275  2c2 11430  3c3 11431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-1cn 10330  ax-addass 10337

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-2 11438  df-3 11439

This theorem is referenced by:  fzo1to4tp  12875  binom3  13304  3lcm2e6woprm  15734  prmgaplem7  16165  2exp16  16196  prmlem1a  16212  23prm  16224  prmlem2  16225  83prm  16228  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem4  16239  1259prm  16241  2503lem2  16243  2503lem3  16244  4001lem2  16247  quart1lem  25033  log2ublem3  25127  log2ub  25128  pntibndlem2  25732  1kp2ke3k  27878  ex-ind-dvds  27893  fib4  31065  ex-decpmul  38160  rabren3dioph  38343  fmtno4nprmfac193  42511  139prmALT  42536  127prm  42540  nnsum4primesodd  42713  nnsum4primesoddALTV  42714