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 12385

Description: 1 + 2 = 3. For a shorter proof using addcomli 11436, see 1p2e3ALT 12386. (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 12305	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7431	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11196	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11254	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12367	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7430	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12384	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2756	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2762	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1534 (class class class)co 7420 1c1 11139 + caddc 11141 2c2 12297 3c3 12298

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-1cn 11196 ax-addass 11203

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-iota 6500 df-fv 6556 df-ov 7423 df-2 12305 df-3 12306

This theorem is referenced by: fzo1to4tp 13752 binom3 14218 3lcm2e6woprm 16585 prmgaplem7 17025 2exp16 17059 prmlem1a 17075 23prm 17087 prmlem2 17088 83prm 17091 139prm 17092 163prm 17093 317prm 17094 631prm 17095 1259lem4 17102 1259prm 17104 2503lem2 17106 2503lem3 17107 4001lem2 17110 quart1lem 26786 log2ublem3 26879 log2ub 26880 pntibndlem2 27523 1kp2ke3k 30255 ex-ind-dvds 30270 fib4 34024 2np3bcnp1 41616 2xp3dxp2ge1d 41693 ex-decpmul 41868 sn-0ne2 41961 3cubeslem3r 42107 rabren3dioph 42235 fmtno4nprmfac193 46914 139prmALT 46936 127prm 46939 nnsum4primesodd 47136 nnsum4primesoddALTV 47137 ackval1012 47763

W3C validator