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 12391

Description: 1 + 2 = 3. For a shorter proof using addcomli 11435, see 1p2e3ALT 12392. (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 12311	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7424	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11195	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11253	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12373	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7423	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12390	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2757	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2763	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1539 (class class class)co 7413 1c1 11138 + caddc 11140 2c2 12303 3c3 12304

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2706 ax-1cn 11195 ax-addass 11202

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2713 df-cleq 2726 df-clel 2808 df-rab 3420 df-v 3465 df-dif 3934 df-un 3936 df-ss 3948 df-nul 4314 df-if 4506 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-br 5124 df-iota 6494 df-fv 6549 df-ov 7416 df-2 12311 df-3 12312

This theorem is referenced by: fzo1to4tp 13775 binom3 14245 3lcm2e6woprm 16634 prmgaplem7 17077 2exp16 17110 prmlem1a 17126 23prm 17138 prmlem2 17139 83prm 17142 139prm 17143 163prm 17144 317prm 17145 631prm 17146 1259lem4 17153 1259prm 17155 2503lem2 17157 2503lem3 17158 4001lem2 17161 quart1lem 26834 log2ublem3 26927 log2ub 26928 pntibndlem2 27571 1kp2ke3k 30393 ex-ind-dvds 30408 fib4 34365 2np3bcnp1 42104 2xp3dxp2ge1d 42201 ex-decpmul 42303 sn-0ne2 42399 3cubeslem3r 42661 rabren3dioph 42789 fmtno4nprmfac193 47519 139prmALT 47541 127prm 47544 nnsum4primesodd 47741 nnsum4primesoddALTV 47742 ackval1012 48569

W3C validator