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

Theorem 3p2e5 11596
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 11501 . . . . 5 2 = (1 + 1)
21oveq2i 6985 . . . 4 (3 + 2) = (3 + (1 + 1))
3 3cn 11519 . . . . 5 3 ∈ ℂ
4 ax-1cn 10391 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10448 . . . 4 ((3 + 1) + 1) = (3 + (1 + 1))
62, 5eqtr4i 2798 . . 3 (3 + 2) = ((3 + 1) + 1)
7 df-4 11503 . . . 4 4 = (3 + 1)
87oveq1i 6984 . . 3 (4 + 1) = ((3 + 1) + 1)
96, 8eqtr4i 2798 . 2 (3 + 2) = (4 + 1)
10 df-5 11504 . 2 5 = (4 + 1)
119, 10eqtr4i 2798 1 (3 + 2) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1508  (class class class)co 6974  1c1 10334   + caddc 10336  2c2 11493  3c3 11494  4c4 11495  5c5 11496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-1cn 10391  ax-addcl 10393  ax-addass 10398
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-rex 3087  df-rab 3090  df-v 3410  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-2 11501  df-3 11502  df-4 11503  df-5 11504
This theorem is referenced by:  3p3e6  11597  2exp16  16278  prmlem1a  16294  5prm  16296  prmlem2  16307  1259lem1  16318  1259lem4  16321  1259prm  16323  4001lem1  16328  4001lem4  16331  birthday  25249  ppiub  25497  bposlem6  25582  bposlem9  25585  2lgsoddprmlem3d  25706  ex-mod  28021  fib5  31341  hgt750lem2  31603  kur14lem8  32082  problem1  32465  235t711  38647  fmtnorec2  43107  fmtno5lem4  43120  257prm  43125  fmtno4nprmfac193  43138  2exp5  43157  41prothprmlem2  43185  linevalexample  43851
  Copyright terms: Public domain W3C validator