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

Theorem 3p2e5 11780
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 11692 . . . . 5 2 = (1 + 1)
21oveq2i 7150 . . . 4 (3 + 2) = (3 + (1 + 1))
3 3cn 11710 . . . . 5 3 ∈ ℂ
4 ax-1cn 10588 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10644 . . . 4 ((3 + 1) + 1) = (3 + (1 + 1))
62, 5eqtr4i 2827 . . 3 (3 + 2) = ((3 + 1) + 1)
7 df-4 11694 . . . 4 4 = (3 + 1)
87oveq1i 7149 . . 3 (4 + 1) = ((3 + 1) + 1)
96, 8eqtr4i 2827 . 2 (3 + 2) = (4 + 1)
10 df-5 11695 . 2 5 = (4 + 1)
119, 10eqtr4i 2827 1 (3 + 2) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7139  1c1 10531   + caddc 10533  2c2 11684  3c3 11685  4c4 11686  5c5 11687
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-addcl 10590  ax-addass 10595
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-2 11692  df-3 11693  df-4 11694  df-5 11695
This theorem is referenced by:  3p3e6  11781  2exp5  16416  2exp16  16420  prmlem1a  16436  5prm  16438  prmlem2  16449  1259lem1  16460  1259lem4  16463  1259prm  16465  4001lem1  16470  4001lem4  16473  birthday  25544  ppiub  25792  bposlem6  25877  bposlem9  25880  2lgsoddprmlem3d  26001  ex-mod  28238  cyc3conja  30853  fib5  31777  hgt750lem2  32037  kur14lem8  32574  problem1  33022  235t711  39482  3cubeslem3l  39624  3cubeslem3r  39625  fmtnorec2  44057  fmtno5lem4  44070  257prm  44075  fmtno4nprmfac193  44088  41prothprmlem2  44133  linevalexample  44801  ackval2012  45102  ackval3012  45103
  Copyright terms: Public domain W3C validator