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

Theorem 5p3e8 11354
Description: 5 + 3 = 8. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
5p3e8 (5 + 3) = 8

Proof of Theorem 5p3e8
StepHypRef Expression
1 df-3 11268 . . . 4 3 = (2 + 1)
21oveq2i 6820 . . 3 (5 + 3) = (5 + (2 + 1))
3 5cn 11288 . . . 4 5 ∈ ℂ
4 2cn 11279 . . . 4 2 ∈ ℂ
5 ax-1cn 10182 . . . 4 1 ∈ ℂ
63, 4, 5addassi 10236 . . 3 ((5 + 2) + 1) = (5 + (2 + 1))
72, 6eqtr4i 2781 . 2 (5 + 3) = ((5 + 2) + 1)
8 df-8 11273 . . 3 8 = (7 + 1)
9 5p2e7 11353 . . . 4 (5 + 2) = 7
109oveq1i 6819 . . 3 ((5 + 2) + 1) = (7 + 1)
118, 10eqtr4i 2781 . 2 8 = ((5 + 2) + 1)
127, 11eqtr4i 2781 1 (5 + 3) = 8
Colors of variables: wff setvar class
Syntax hints:   = wceq 1628  (class class class)co 6809  1c1 10125   + caddc 10127  2c2 11258  3c3 11259  5c5 11261  7c7 11263  8c8 11264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-addass 10189  ax-i2m1 10192  ax-1ne0 10193  ax-rrecex 10196  ax-cnre 10197
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-iota 6008  df-fv 6053  df-ov 6812  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273
This theorem is referenced by:  5p4e9  11355  ef01bndlem  15109  2exp16  15995  1259lem2  16037  log2ublem3  24870  log2ub  24871  bposlem8  25211  lgsdir2lem1  25245  fib6  30773  fmtno5lem2  41972  fmtno5lem4  41974  257prm  41979  gbpart8  42162  8gbe  42167  evengpop3  42192
  Copyright terms: Public domain W3C validator