Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  6p2e8 Structured version   Visualization version   GIF version

Theorem 6p2e8 11789
 Description: 6 + 2 = 8. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
6p2e8 (6 + 2) = 8

Proof of Theorem 6p2e8
StepHypRef Expression
1 df-2 11693 . . . . 5 2 = (1 + 1)
21oveq2i 7156 . . . 4 (6 + 2) = (6 + (1 + 1))
3 6cn 11721 . . . . 5 6 ∈ ℂ
4 ax-1cn 10587 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10643 . . . 4 ((6 + 1) + 1) = (6 + (1 + 1))
62, 5eqtr4i 2850 . . 3 (6 + 2) = ((6 + 1) + 1)
7 df-7 11698 . . . 4 7 = (6 + 1)
87oveq1i 7155 . . 3 (7 + 1) = ((6 + 1) + 1)
96, 8eqtr4i 2850 . 2 (6 + 2) = (7 + 1)
10 df-8 11699 . 2 8 = (7 + 1)
119, 10eqtr4i 2850 1 (6 + 2) = 8
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  (class class class)co 7145  1c1 10530   + caddc 10532  2c2 11685  6c6 11689  7c7 11690  8c8 11691 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796  ax-1cn 10587  ax-addcl 10589  ax-addass 10594 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4550  df-pr 4552  df-op 4556  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7148  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699 This theorem is referenced by:  6p3e9  11790  6t3e18  12196  83prm  16452  1259lem2  16461  1259lem5  16464  2503lem2  16467  2503lem3  16468  4001lem1  16470  log2ub  25531  hgt750lem2  31948  3cubeslem3l  39480  resqrtvalex  40198  imsqrtvalex  40199  lhe4.4ex1a  40890  fmtno5faclem3  43961
 Copyright terms: Public domain W3C validator