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 12354

Description: 1 + 2 = 3. For a shorter proof using addcomli 11405, see 1p2e3ALT 12355. (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 12274	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7413	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11165	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11223	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12336	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7412	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12353	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2752	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2758	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1533 (class class class)co 7402 1c1 11108 + caddc 11110 2c2 12266 3c3 12267

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 ax-1cn 11165 ax-addass 11172

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-iota 6486 df-fv 6542 df-ov 7405 df-2 12274 df-3 12275

This theorem is referenced by: fzo1to4tp 13721 binom3 14188 3lcm2e6woprm 16555 prmgaplem7 16995 2exp16 17029 prmlem1a 17045 23prm 17057 prmlem2 17058 83prm 17061 139prm 17062 163prm 17063 317prm 17064 631prm 17065 1259lem4 17072 1259prm 17074 2503lem2 17076 2503lem3 17077 4001lem2 17080 quart1lem 26727 log2ublem3 26820 log2ub 26821 pntibndlem2 27464 1kp2ke3k 30193 ex-ind-dvds 30208 fib4 33922 2np3bcnp1 41493 2xp3dxp2ge1d 41555 ex-decpmul 41736 sn-0ne2 41829 3cubeslem3r 41975 rabren3dioph 42103 fmtno4nprmfac193 46787 139prmALT 46809 127prm 46812 nnsum4primesodd 47009 nnsum4primesoddALTV 47010 ackval1012 47624

W3C validator