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

Theorem 5p2e7 10009
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 9951 . . . . 5  |-  2  =  ( 1  +  1 )
21oveq2i 5992 . . . 4  |-  ( 5  +  2 )  =  ( 5  +  ( 1  +  1 ) )
3 5re 9968 . . . . . 6  |-  5  e.  RR
43recni 8996 . . . . 5  |-  5  e.  CC
5 ax-1cn 8942 . . . . 5  |-  1  e.  CC
64, 5, 5addassi 8992 . . . 4  |-  ( ( 5  +  1 )  +  1 )  =  ( 5  +  ( 1  +  1 ) )
72, 6eqtr4i 2389 . . 3  |-  ( 5  +  2 )  =  ( ( 5  +  1 )  +  1 )
8 df-6 9955 . . . 4  |-  6  =  ( 5  +  1 )
98oveq1i 5991 . . 3  |-  ( 6  +  1 )  =  ( ( 5  +  1 )  +  1 )
107, 9eqtr4i 2389 . 2  |-  ( 5  +  2 )  =  ( 6  +  1 )
11 df-7 9956 . 2  |-  7  =  ( 6  +  1 )
1210, 11eqtr4i 2389 1  |-  ( 5  +  2 )  =  7
Colors of variables: wff set class
Syntax hints:    = wceq 1647  (class class class)co 5981   1c1 8885    + caddc 8887   2c2 9942   5c5 9945   6c6 9946   7c7 9947
This theorem is referenced by:  5p3e8  10010  17prm  13326  prmlem2  13329  37prm  13330  317prm  13335  1259lem1  13337  1259lem2  13338  1259lem4  13340  2503lem2  13344  4001lem1  13347  4001lem4  13350  log2ub  20467  bposlem8  20753
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-addass 8949  ax-i2m1 8952  ax-1ne0 8953  ax-rrecex 8956  ax-cnre 8957
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984  df-2 9951  df-3 9952  df-4 9953  df-5 9954  df-6 9955  df-7 9956
  Copyright terms: Public domain W3C validator