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 12436

Description: 1 + 2 = 3. For a shorter proof using addcomli 11482, see 1p2e3ALT 12437. (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 12356	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7459	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11300	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12418	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7458	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12435	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2768	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2774	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1537 (class class class)co 7448 1c1 11185 + caddc 11187 2c2 12348 3c3 12349

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2711 ax-1cn 11242 ax-addass 11249

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-sb 2065 df-clab 2718 df-cleq 2732 df-clel 2819 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-iota 6525 df-fv 6581 df-ov 7451 df-2 12356 df-3 12357

This theorem is referenced by: fzo1to4tp 13804 binom3 14273 3lcm2e6woprm 16662 prmgaplem7 17104 2exp16 17138 prmlem1a 17154 23prm 17166 prmlem2 17167 83prm 17170 139prm 17171 163prm 17172 317prm 17173 631prm 17174 1259lem4 17181 1259prm 17183 2503lem2 17185 2503lem3 17186 4001lem2 17189 quart1lem 26916 log2ublem3 27009 log2ub 27010 pntibndlem2 27653 1kp2ke3k 30478 ex-ind-dvds 30493 fib4 34369 2np3bcnp1 42101 2xp3dxp2ge1d 42198 ex-decpmul 42294 sn-0ne2 42382 3cubeslem3r 42643 rabren3dioph 42771 fmtno4nprmfac193 47448 139prmALT 47470 127prm 47473 nnsum4primesodd 47670 nnsum4primesoddALTV 47671 ackval1012 48424

W3C validator