Theorem 1p2e3 12492

Description: 1 + 2 = 3. For a shorter proof using addcomli 11509, see 1p2e3ALT 12493. (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 12412	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11265	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11326	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12473	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7434	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12491	. . 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 1569  (class class class)co 7424  1c1 11208   + caddc 11210  2c2 12404  3c3 12405

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-addass 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-2 12412  df-3 12413

This theorem is used by:  fzo1to4tp  13896  binom3  14375  3lcm2e6woprm  16799  prmgaplem7  17244  2exp16  17277  prmlem1a  17293  23prm  17306  prmlem2  17307  83prm  17310  139prm  17311  163prm  17312  317prm  17313  631prm  17314  1259lem4  17321  1259prm  17323  2503lem2  17325  2503lem3  17326  4001lem2  17329  quart1lem  27192  log2ublem3  27285  log2ub  27286  pntibndlem2  27927  1kp2ke3k  31056  ex-ind-dvds  31071  cos9thpiminplylem2  34465  fib4  35086  2np3bcnp1  43303  1p3e4  43419  2p3e5  43425  ex-decpmul  43472  sn-0ne2  43566  3cubeslem3r  43806  rabren3dioph  43931  cos3t  48026  modm2nep1  48550  fmtno4nprmfac193  48767  139prmALT  48789  127prm  48792  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  pgnbgreunbgrlem2lem1  49320  gpg5edgnedg  49336  ackval1012  49910  crosspdotsumlem  51147  crosspaltd  51149  crossp3d  51150