Theorem 4p2e6 11870

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 11780	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7182	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 11802	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 10674	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 10730	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2764	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 11783	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7181	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2764	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 11784	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2764	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1542  (class class class)co 7171  1c1 10617   + caddc 10619  2c2 11772  4c4 11774  5c5 11775  6c6 11776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-1cn 10674  ax-addcl 10676  ax-addass 10681

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7174  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784

This theorem is referenced by:  4p3e7  11871  div4p1lem1div2  11972  4t4e16  12279  6gcd4e2  15983  2exp16  16528  163prm  16562  631prm  16564  1259lem4  16571  2503lem2  16575  2503lem3  16576  4001lem1  16578  4001lem2  16579  4001lem4  16581  bposlem9  26028  hgt750lem2  32202  3exp7  39678  3lexlogpow5ineq1  39679  aks4d1p1p5  39699  235t711  39887  ex-decpmul  39888  3cubeslem3r  40073  lhe4.4ex1a  41477  fmtno4prmfac  44550  fmtno5faclem1  44557  gbowgt5  44740  mogoldbb  44763