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 12046

Description: 1 + 2 = 3. For a shorter proof using addcomli 11097, see 1p2e3ALT 12047. (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 11966	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7266	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 10916	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12028	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7265	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12045	. . 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 7255 1c1 10803 + caddc 10805 2c2 11958 3c3 11959

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-ext 2709 ax-1cn 10860 ax-addass 10867

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-iota 6376 df-fv 6426 df-ov 7258 df-2 11966 df-3 11967

This theorem is referenced by: fzo1to4tp 13403 binom3 13867 3lcm2e6woprm 16248 prmgaplem7 16686 2exp16 16720 prmlem1a 16736 23prm 16748 prmlem2 16749 83prm 16752 139prm 16753 163prm 16754 317prm 16755 631prm 16756 1259lem4 16763 1259prm 16765 2503lem2 16767 2503lem3 16768 4001lem2 16771 quart1lem 25910 log2ublem3 26003 log2ub 26004 pntibndlem2 26644 1kp2ke3k 28711 ex-ind-dvds 28726 fib4 32271 2np3bcnp1 40028 2xp3dxp2ge1d 40090 ex-decpmul 40241 sn-0ne2 40310 3cubeslem3r 40425 rabren3dioph 40553 fmtno4nprmfac193 44914 139prmALT 44936 127prm 44939 nnsum4primesodd 45136 nnsum4primesoddALTV 45137 ackval1012 45924

W3C validator