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

Theorem 3p2e5 12417
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 12329 . . . . 5 2 = (1 + 1)
21oveq2i 7442 . . . 4 (3 + 2) = (3 + (1 + 1))
3 3cn 12347 . . . . 5 3 ∈ ℂ
4 ax-1cn 11213 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 11271 . . . 4 ((3 + 1) + 1) = (3 + (1 + 1))
62, 5eqtr4i 2768 . . 3 (3 + 2) = ((3 + 1) + 1)
7 df-4 12331 . . . 4 4 = (3 + 1)
87oveq1i 7441 . . 3 (4 + 1) = ((3 + 1) + 1)
96, 8eqtr4i 2768 . 2 (3 + 2) = (4 + 1)
10 df-5 12332 . 2 5 = (4 + 1)
119, 10eqtr4i 2768 1 (3 + 2) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7431  1c1 11156   + caddc 11158  2c2 12321  3c3 12322  4c4 12323  5c5 12324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215  ax-addass 11220
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329  df-3 12330  df-4 12331  df-5 12332
This theorem is referenced by:  3p3e6  12418  fz0to5un2tp  13671  2exp5  17123  2exp16  17128  prmlem1a  17144  5prm  17146  prmlem2  17157  1259lem1  17168  1259lem4  17171  1259prm  17173  4001lem1  17178  4001lem4  17181  birthday  26997  ppiub  27248  bposlem6  27333  bposlem9  27336  2lgsoddprmlem3d  27457  ex-mod  30468  cyc3conja  33177  fib5  34407  hgt750lem2  34667  kur14lem8  35218  problem1  35670  235t711  42339  3cubeslem3l  42697  3cubeslem3r  42698  fmtnorec2  47530  fmtno5lem4  47543  257prm  47548  fmtno4nprmfac193  47561  41prothprmlem2  47605  linevalexample  48312  ackval2012  48612  ackval3012  48613
  Copyright terms: Public domain W3C validator