Theorem 4p2e6 12340

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 12250	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7400	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12272	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11132	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11190	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2756	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12253	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7399	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2756	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12254	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2756	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1540  (class class class)co 7389  1c1 11075   + caddc 11077  2c2 12242  4c4 12244  5c5 12245  6c6 12246

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 2702  ax-1cn 11132  ax-addcl 11134  ax-addass 11139

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-2 12250  df-3 12251  df-4 12252  df-5 12253  df-6 12254

This theorem is referenced by:  4p3e7  12341  div4p1lem1div2  12443  4t4e16  12754  6gcd4e2  16514  2exp16  17067  163prm  17101  631prm  17103  1259lem4  17110  2503lem2  17114  2503lem3  17115  4001lem1  17117  4001lem2  17118  4001lem4  17120  bposlem9  27209  hgt750lem2  34649  3exp7  42036  3lexlogpow5ineq1  42037  aks4d1p1p5  42058  235t711  42288  ex-decpmul  42289  3cubeslem3r  42668  lhe4.4ex1a  44311  ceil5half3  47331  fmtno4prmfac  47563  fmtno5faclem1  47570  gbowgt5  47753  mogoldbb  47776