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

Theorem 3p2e5 11372
Description: 3 + 2 = 5. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
3p2e5 (3 + 2) = 5

Proof of Theorem 3p2e5
StepHypRef Expression
1 df-2 11291 . . . . 5 2 = (1 + 1)
21oveq2i 6825 . . . 4 (3 + 2) = (3 + (1 + 1))
3 3cn 11307 . . . . 5 3 ∈ ℂ
4 ax-1cn 10206 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10260 . . . 4 ((3 + 1) + 1) = (3 + (1 + 1))
62, 5eqtr4i 2785 . . 3 (3 + 2) = ((3 + 1) + 1)
7 df-4 11293 . . . 4 4 = (3 + 1)
87oveq1i 6824 . . 3 (4 + 1) = ((3 + 1) + 1)
96, 8eqtr4i 2785 . 2 (3 + 2) = (4 + 1)
10 df-5 11294 . 2 5 = (4 + 1)
119, 10eqtr4i 2785 1 (3 + 2) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6814  1c1 10149   + caddc 10151  2c2 11282  3c3 11283  4c4 11284  5c5 11285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-addass 10213  ax-i2m1 10216  ax-1ne0 10217  ax-rrecex 10220  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-2 11291  df-3 11292  df-4 11293  df-5 11294
This theorem is referenced by:  3p3e6  11373  2exp16  16019  prmlem1a  16035  5prm  16037  prmlem2  16049  1259lem1  16060  1259lem4  16063  1259prm  16065  4001lem1  16070  4001lem4  16073  birthday  24901  ppiub  25149  bposlem6  25234  bposlem9  25237  2lgsoddprmlem3d  25358  ex-mod  27638  fib5  30797  hgt750lem2  31060  kur14lem8  31523  problem1  31886  fmtnorec2  41983  fmtno5lem4  41996  257prm  42001  fmtno4nprmfac193  42014  2exp5  42035  41prothprmlem2  42063  linevalexample  42712
  Copyright terms: Public domain W3C validator