Theorem 1p2e3 12525

Description: 1 + 2 = 3. For a shorter proof using addcomli 11541, see 1p2e3ALT 12526. (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 12445	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7462	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11358	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12506	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7461	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12524	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2786	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2792	1 ⊢ (1 + 2) = 3

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  3c3 12438

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addass 11304

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446

This theorem is used by:  fzo1to4tp  13929  binom3  14409  3lcm2e6woprm  16834  prmgaplem7  17279  2exp16  17312  prmlem1a  17328  23prm  17341  prmlem2  17342  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem4  17356  1259prm  17358  2503lem2  17360  2503lem3  17361  4001lem2  17364  quart1lem  27240  log2ublem3  27333  log2ub  27334  pntibndlem2  27975  1kp2ke3k  31104  ex-ind-dvds  31119  cos9thpiminplylem2  34526  fib4  35147  2np3bcnp1  43460  1p3e4  43576  2p3e5  43582  ex-decpmul  43629  sn-0ne2  43723  3cubeslem3r  43963  rabren3dioph  44088  cos3t  48191  modm2nep1  48715  fmtno4nprmfac193  48932  139prmALT  48954  127prm  48957  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  pgnbgreunbgrlem2lem1  49485  gpg5edgnedg  49501  ackval1012  50133  crosspdotsumlem  51392  crosspaltd  51394  crossp3d  51395