Theorem 1p2e3 12478

Description: 1 + 2 = 3. For a shorter proof using addcomli 11495, see 1p2e3ALT 12479. (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 12398	. . 3 ⊢ 2 = (1 + 1)
2	1	oveq2i 7429	. 2 ⊢ (1 + 2) = (1 + (1 + 1))
3		ax-1cn 11251	. . 3 ⊢ 1 ∈ ℂ
4	3, 3, 3	addassi 11312	. 2 ⊢ ((1 + 1) + 1) = (1 + (1 + 1))
5		1p1e2 12459	. . . 4 ⊢ (1 + 1) = 2
6	5	oveq1i 7428	. . 3 ⊢ ((1 + 1) + 1) = (2 + 1)
7		2p1e3 12477	. . 3 ⊢ (2 + 1) = 3
8	6, 7	eqtri 2784	. 2 ⊢ ((1 + 1) + 1) = 3
9	2, 4, 8	3eqtr2i 2790	1 ⊢ (1 + 2) = 3

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  2c2 12390  3c3 12391

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-addass 11258

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-2 12398  df-3 12399

This theorem is used by:  fzo1to4tp  13882  binom3  14361  3lcm2e6woprm  16783  prmgaplem7  17228  2exp16  17261  prmlem1a  17277  23prm  17290  prmlem2  17291  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem4  17305  1259prm  17307  2503lem2  17309  2503lem3  17310  4001lem2  17313  quart1lem  27176  log2ublem3  27269  log2ub  27270  pntibndlem2  27911  1kp2ke3k  31040  ex-ind-dvds  31055  cos9thpiminplylem2  34408  fib4  35029  2np3bcnp1  43174  1p3e4  43290  2p3e5  43296  ex-decpmul  43343  sn-0ne2  43437  3cubeslem3r  43677  rabren3dioph  43801  cos3t  47887  modm2nep1  48411  fmtno4nprmfac193  48628  139prmALT  48650  127prm  48653  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  pgnbgreunbgrlem2lem1  49181  gpg5edgnedg  49197  ackval1012  49771  crosspdotsumlem  50933  crosspaltd  50935  crossp3d  50936