Theorem 1p2e3 12300

Description: 1 + 2 = 3. For a shorter proof using addcomli 11342, see 1p2e3ALT 12301. (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 12225	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7380	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11160	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12282	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7379	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12299	. . 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 7369  1c1 11045   + caddc 11047  2c2 12217  3c3 12218

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 11102  ax-addass 11109

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225  df-3 12226

This theorem is referenced by:  fzo1to4tp  13691  binom3  14165  3lcm2e6woprm  16561  prmgaplem7  17004  2exp16  17037  prmlem1a  17053  23prm  17065  prmlem2  17066  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem4  17080  1259prm  17082  2503lem2  17084  2503lem3  17085  4001lem2  17088  quart1lem  26798  log2ublem3  26891  log2ub  26892  pntibndlem2  27535  1kp2ke3k  30425  ex-ind-dvds  30440  cos9thpiminplylem2  33766  fib4  34388  2np3bcnp1  42125  1p3e4  42240  ex-decpmul  42287  sn-0ne2  42387  3cubeslem3r  42668  rabren3dioph  42796  modm2nep1  47360  fmtno4nprmfac193  47568  139prmALT  47590  127prm  47593  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  pgnbgreunbgrlem2lem1  48097  ackval1012  48672