Theorem 4p2e6 12535

Description: 4 + 2 = 6. (Contributed by NM, 11-May-2004.)

Assertion

Ref	Expression
4p2e6	⊢ (4 + 2) = 6

Proof of Theorem 4p2e6

Step	Hyp	Ref	Expression
1		df-2 12445	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7462	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12468	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11297	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11358	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2789	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12448	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7461	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2789	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12449	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2789	1 ⊢ (4 + 2) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7451  1c1 11240   + caddc 11242  2c2 12437  4c4 12439  5c5 12440  6c6 12441

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299  ax-addass 11304

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449

This theorem is used by:  4p3e7  12536  div4p1lem1div2  12641  4t4e16  12958  6gcd4e2  16755  2exp16  17312  163prm  17347  631prm  17349  1259lem4  17356  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem2  17364  4001lem4  17366  bposlem9  27676  hgt750lem2  35392  3exp7  43369  3lexlogpow5ineq1  43370  aks4d1p1p5  43391  4p4e8ALT  43575  2p4e6  43583  235t711  43628  ex-decpmul  43629  3cubeslem3r  43963  lhe4.4ex1a  45574  ceil5half3  48689  fmtno4prmfac  48930  fmtno5faclem1  48937  gbowgt5  49133  mogoldbb  49156