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

Theorem 4p3e7 12240
Description: 4 + 3 = 7. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
4p3e7 (4 + 3) = 7

Proof of Theorem 4p3e7
StepHypRef Expression
1 df-3 12150 . . . 4 3 = (2 + 1)
21oveq2i 7360 . . 3 (4 + 3) = (4 + (2 + 1))
3 4cn 12171 . . . 4 4 ∈ ℂ
4 2cn 12161 . . . 4 2 ∈ ℂ
5 ax-1cn 11042 . . . 4 1 ∈ ℂ
63, 4, 5addassi 11098 . . 3 ((4 + 2) + 1) = (4 + (2 + 1))
72, 6eqtr4i 2768 . 2 (4 + 3) = ((4 + 2) + 1)
8 df-7 12154 . . 3 7 = (6 + 1)
9 4p2e6 12239 . . . 4 (4 + 2) = 6
109oveq1i 7359 . . 3 ((4 + 2) + 1) = (6 + 1)
118, 10eqtr4i 2768 . 2 7 = ((4 + 2) + 1)
127, 11eqtr4i 2768 1 (4 + 3) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  (class class class)co 7349  1c1 10985   + caddc 10987  2c2 12141  3c3 12142  4c4 12143  6c6 12145  7c7 12146
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-1cn 11042  ax-addcl 11044  ax-addass 11049
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6443  df-fv 6499  df-ov 7352  df-2 12149  df-3 12150  df-4 12151  df-5 12152  df-6 12153  df-7 12154
This theorem is referenced by:  4p4e8  12241  37prm  16927  317prm  16932  1259lem5  16941  2503lem2  16944  4001lem1  16947  4001lem2  16948  log2ub  26221  bposlem8  26561  2lgslem3d  26669  2lgsoddprmlem3d  26683  hgt750lem  33037  hgt750lem2  33038  fmtno5lem4  45497  257prm  45502  127prm  45540  gbpart7  45708  sbgoldbwt  45718  sbgoldbst  45719  ackval2012  46526
  Copyright terms: Public domain W3C validator