Theorem 1p2e3 12266

Description: 1 + 2 = 3. For a shorter proof using addcomli 11308, see 1p2e3ALT 12267. (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 12191	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7360	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11067	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11125	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12248	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7359	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12265	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2752	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2758	1 ⊢ (1 + 2) = 3

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  2c2 12183  3c3 12184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-addass 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192

This theorem is referenced by:  fzo1to4tp  13657  binom3  14131  3lcm2e6woprm  16526  prmgaplem7  16969  2exp16  17002  prmlem1a  17018  23prm  17030  prmlem2  17031  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem4  17045  1259prm  17047  2503lem2  17049  2503lem3  17050  4001lem2  17053  quart1lem  26763  log2ublem3  26856  log2ub  26857  pntibndlem2  27500  1kp2ke3k  30390  ex-ind-dvds  30405  cos9thpiminplylem2  33750  fib4  34372  2np3bcnp1  42117  1p3e4  42232  ex-decpmul  42279  sn-0ne2  42379  3cubeslem3r  42660  rabren3dioph  42788  modm2nep1  47350  fmtno4nprmfac193  47558  139prmALT  47580  127prm  47583  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  pgnbgreunbgrlem2lem1  48098  gpg5edgnedg  48114  ackval1012  48675