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

Theorem 7p2e9 11795
Description: 7 + 2 = 9. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
7p2e9 (7 + 2) = 9

Proof of Theorem 7p2e9
StepHypRef Expression
1 df-2 11697 . . . . 5 2 = (1 + 1)
21oveq2i 7160 . . . 4 (7 + 2) = (7 + (1 + 1))
3 7cn 11728 . . . . 5 7 ∈ ℂ
4 ax-1cn 10593 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10649 . . . 4 ((7 + 1) + 1) = (7 + (1 + 1))
62, 5eqtr4i 2850 . . 3 (7 + 2) = ((7 + 1) + 1)
7 df-8 11703 . . . 4 8 = (7 + 1)
87oveq1i 7159 . . 3 (8 + 1) = ((7 + 1) + 1)
96, 8eqtr4i 2850 . 2 (7 + 2) = (8 + 1)
10 df-9 11704 . 2 9 = (8 + 1)
119, 10eqtr4i 2850 1 (7 + 2) = 9
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  (class class class)co 7149  1c1 10536   + caddc 10538  2c2 11689  7c7 11694  8c8 11695  9c9 11696
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10593  ax-addcl 10595  ax-addass 10600
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704
This theorem is referenced by:  7p3e10  12170  7t7e49  12209  cos2bnd  15541  prmlem2  16453  139prm  16457  1259lem2  16465  1259lem3  16466  1259lem4  16467  1259lem5  16468  2503lem2  16471  4001lem4  16477  hgt750lem2  31983  fmtno5lem4  44003  fmtno5fac  44029  139prmALT  44043
  Copyright terms: Public domain W3C validator