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 12406

Description: 1 + 2 = 3. For a shorter proof using addcomli 11450, see 1p2e3ALT 12407. (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 12326	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7441	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11268	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12388	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7440	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12405	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2762	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2768	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1536 (class class class)co 7430 1c1 11153 + caddc 11155 2c2 12318 3c3 12319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-1cn 11210 ax-addass 11217

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-iota 6515 df-fv 6570 df-ov 7433 df-2 12326 df-3 12327

This theorem is referenced by: fzo1to4tp 13789 binom3 14259 3lcm2e6woprm 16648 prmgaplem7 17090 2exp16 17124 prmlem1a 17140 23prm 17152 prmlem2 17153 83prm 17156 139prm 17157 163prm 17158 317prm 17159 631prm 17160 1259lem4 17167 1259prm 17169 2503lem2 17171 2503lem3 17172 4001lem2 17175 quart1lem 26912 log2ublem3 27005 log2ub 27006 pntibndlem2 27649 1kp2ke3k 30474 ex-ind-dvds 30489 fib4 34385 2np3bcnp1 42125 2xp3dxp2ge1d 42222 ex-decpmul 42318 sn-0ne2 42412 3cubeslem3r 42674 rabren3dioph 42802 fmtno4nprmfac193 47498 139prmALT 47520 127prm 47523 nnsum4primesodd 47720 nnsum4primesoddALTV 47721 ackval1012 48539

W3C validator