Theorem 4p2e6 12392

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 12302	. . . . 5 ⊢ 2 = (1 + 1)
2	1	oveq2i 7422	. . . 4 ⊢ (4 + 2) = (4 + (1 + 1))
3		4cn 12325	. . . . 5 ⊢ 4 ∈ ℂ
4		ax-1cn 11157	. . . . 5 ⊢ 1 ∈ ℂ
5	3, 4, 4	addassi 11218	. . . 4 ⊢ ((4 + 1) + 1) = (4 + (1 + 1))
6	2, 5	eqtr4i 2795	. . 3 ⊢ (4 + 2) = ((4 + 1) + 1)
7		df-5 12305	. . . 4 ⊢ 5 = (4 + 1)
8	7	oveq1i 7421	. . 3 ⊢ (5 + 1) = ((4 + 1) + 1)
9	6, 8	eqtr4i 2795	. 2 ⊢ (4 + 2) = (5 + 1)
10		df-6 12306	. 2 ⊢ 6 = (5 + 1)
11	9, 10	eqtr4i 2795	1 ⊢ (4 + 2) = 6

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11100   + caddc 11102  2c2 12294  4c4 12296  5c5 12297  6c6 12298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-addcl 11159  ax-addass 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12302  df-3 12303  df-4 12304  df-5 12305  df-6 12306

This theorem is referenced by:  4p3e7  12393  div4p1lem1div2  12498  4t4e16  12814  6gcd4e2  16595  2exp16  17149  163prm  17184  631prm  17186  1259lem4  17193  2503lem2  17197  2503lem3  17198  4001lem1  17200  4001lem2  17201  4001lem4  17203  bposlem9  27421  hgt750lem2  34983  3exp7  42709  3lexlogpow5ineq1  42710  aks4d1p1p5  42731  235t711  42955  ex-decpmul  42956  3cubeslem3r  43309  lhe4.4ex1a  44930  ceil5half3  47971  fmtno4prmfac  48212  fmtno5faclem1  48219  gbowgt5  48415  mogoldbb  48438