Theorem 4p2e6 12401

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 12311	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7435	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12333	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11202	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11260	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2758	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12314	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7434	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2758	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12315	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2758	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1533  (class class class)co 7424  1c1 11145   + caddc 11147  2c2 12303  4c4 12305  5c5 12306  6c6 12307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-1cn 11202  ax-addcl 11204  ax-addass 11209

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-iota 6503  df-fv 6559  df-ov 7427  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315

This theorem is referenced by:  4p3e7  12402  div4p1lem1div2  12503  4t4e16  12812  6gcd4e2  16519  2exp16  17065  163prm  17099  631prm  17101  1259lem4  17108  2503lem2  17112  2503lem3  17113  4001lem1  17115  4001lem2  17116  4001lem4  17118  bposlem9  27243  hgt750lem2  34289  3exp7  41528  3lexlogpow5ineq1  41529  aks4d1p1p5  41550  235t711  41870  ex-decpmul  41871  3cubeslem3r  42110  lhe4.4ex1a  43769  fmtno4prmfac  46914  fmtno5faclem1  46921  gbowgt5  47104  mogoldbb  47127