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 12362

Description: 1 + 2 = 3. For a shorter proof using addcomli 11413, see 1p2e3ALT 12363. (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 12282	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7423	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11174	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11231	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12344	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7422	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12361	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2759	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2765	1 ⊢ (1 + 2) = 3

Colors of variables: wff setvar class

Syntax hints: = wceq 1540 (class class class)co 7412 1c1 11117 + caddc 11119 2c2 12274 3c3 12275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 ax-1cn 11174 ax-addass 11181

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-ov 7415 df-2 12282 df-3 12283

This theorem is referenced by: fzo1to4tp 13727 binom3 14194 3lcm2e6woprm 16559 prmgaplem7 16997 2exp16 17031 prmlem1a 17047 23prm 17059 prmlem2 17060 83prm 17063 139prm 17064 163prm 17065 317prm 17066 631prm 17067 1259lem4 17074 1259prm 17076 2503lem2 17078 2503lem3 17079 4001lem2 17082 quart1lem 26700 log2ublem3 26793 log2ub 26794 pntibndlem2 27436 1kp2ke3k 30131 ex-ind-dvds 30146 fib4 33866 2np3bcnp1 41426 2xp3dxp2ge1d 41488 ex-decpmul 41668 sn-0ne2 41741 3cubeslem3r 41887 rabren3dioph 42015 fmtno4nprmfac193 46700 139prmALT 46722 127prm 46725 nnsum4primesodd 46922 nnsum4primesoddALTV 46923 ackval1012 47537

W3C validator