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

Theorem 5p2e7 11150
Description: 5 + 2 = 7. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
5p2e7 (5 + 2) = 7

Proof of Theorem 5p2e7
StepHypRef Expression
1 df-2 11064 . . . . 5 2 = (1 + 1)
21oveq2i 6646 . . . 4 (5 + 2) = (5 + (1 + 1))
3 5cn 11085 . . . . 5 5 ∈ ℂ
4 ax-1cn 9979 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10033 . . . 4 ((5 + 1) + 1) = (5 + (1 + 1))
62, 5eqtr4i 2645 . . 3 (5 + 2) = ((5 + 1) + 1)
7 df-6 11068 . . . 4 6 = (5 + 1)
87oveq1i 6645 . . 3 (6 + 1) = ((5 + 1) + 1)
96, 8eqtr4i 2645 . 2 (5 + 2) = (6 + 1)
10 df-7 11069 . 2 7 = (6 + 1)
119, 10eqtr4i 2645 1 (5 + 2) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  (class class class)co 6635  1c1 9922   + caddc 9924  2c2 11055  5c5 11058  6c6 11059  7c7 11060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-addass 9986  ax-i2m1 9989  ax-1ne0 9990  ax-rrecex 9993  ax-cnre 9994
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069
This theorem is referenced by:  5p3e8  11151  17prm  15805  prmlem2  15808  37prm  15809  317prm  15814  1259lem1  15819  1259lem2  15820  1259lem4  15822  2503lem2  15826  4001lem1  15829  4001lem4  15832  log2ub  24657  bposlem8  24997  fmtno5lem2  41231  257prm  41238  127prm  41280
  Copyright terms: Public domain W3C validator