1p2e3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 1p2e3		Structured version Visualization version GIF version

Theorem 1p2e3 12351

Description: 1 + 2 = 3. For a shorter proof using addcomli 11402, see 1p2e3ALT 12352. (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 12271	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7416	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11220	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12333	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7415	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12350	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2760	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2766	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1541 (class class class)co 7405 1c1 11107 + caddc 11109 2c2 12263 3c3 12264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-1cn 11164 ax-addass 11171

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-ov 7408 df-2 12271 df-3 12272

This theorem is referenced by: fzo1to4tp 13716 binom3 14183 3lcm2e6woprm 16548 prmgaplem7 16986 2exp16 17020 prmlem1a 17036 23prm 17048 prmlem2 17049 83prm 17052 139prm 17053 163prm 17054 317prm 17055 631prm 17056 1259lem4 17063 1259prm 17065 2503lem2 17067 2503lem3 17068 4001lem2 17071 quart1lem 26349 log2ublem3 26442 log2ub 26443 pntibndlem2 27083 1kp2ke3k 29688 ex-ind-dvds 29703 fib4 33391 2np3bcnp1 40948 2xp3dxp2ge1d 41010 ex-decpmul 41201 sn-0ne2 41275 3cubeslem3r 41410 rabren3dioph 41538 fmtno4nprmfac193 46228 139prmALT 46250 127prm 46253 nnsum4primesodd 46450 nnsum4primesoddALTV 46451 ackval1012 47329

W3C validator