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 12116

Description: 1 + 2 = 3. For a shorter proof using addcomli 11167, see 1p2e3ALT 12117. (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 12036	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7286	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 10929	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 10985	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12098	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7285	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12115	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2766	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2772	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1539 (class class class)co 7275 1c1 10872 + caddc 10874 2c2 12028 3c3 12029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-1cn 10929 ax-addass 10936

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-iota 6391 df-fv 6441 df-ov 7278 df-2 12036 df-3 12037

This theorem is referenced by: fzo1to4tp 13475 binom3 13939 3lcm2e6woprm 16320 prmgaplem7 16758 2exp16 16792 prmlem1a 16808 23prm 16820 prmlem2 16821 83prm 16824 139prm 16825 163prm 16826 317prm 16827 631prm 16828 1259lem4 16835 1259prm 16837 2503lem2 16839 2503lem3 16840 4001lem2 16843 quart1lem 26005 log2ublem3 26098 log2ub 26099 pntibndlem2 26739 1kp2ke3k 28810 ex-ind-dvds 28825 fib4 32371 2np3bcnp1 40100 2xp3dxp2ge1d 40162 ex-decpmul 40320 sn-0ne2 40389 3cubeslem3r 40509 rabren3dioph 40637 fmtno4nprmfac193 45026 139prmALT 45048 127prm 45051 nnsum4primesodd 45248 nnsum4primesoddALTV 45249 ackval1012 46036

W3C validator