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

Theorem 4p3e7 12241
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 12151 . . . 4 3 = (2 + 1)
21oveq2i 7361 . . 3 (4 + 3) = (4 + (2 + 1))
3 4cn 12172 . . . 4 4 ∈ ℂ
4 2cn 12162 . . . 4 2 ∈ ℂ
5 ax-1cn 11043 . . . 4 1 ∈ ℂ
63, 4, 5addassi 11099 . . 3 ((4 + 2) + 1) = (4 + (2 + 1))
72, 6eqtr4i 2769 . 2 (4 + 3) = ((4 + 2) + 1)
8 df-7 12155 . . 3 7 = (6 + 1)
9 4p2e6 12240 . . . 4 (4 + 2) = 6
109oveq1i 7360 . . 3 ((4 + 2) + 1) = (6 + 1)
118, 10eqtr4i 2769 . 2 7 = ((4 + 2) + 1)
127, 11eqtr4i 2769 1 (4 + 3) = 7
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7350  1c1 10986   + caddc 10988  2c2 12142  3c3 12143  4c4 12144  6c6 12146  7c7 12147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-1cn 11043  ax-addcl 11045  ax-addass 11050
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-iota 6444  df-fv 6500  df-ov 7353  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155
This theorem is referenced by:  4p4e8  12242  37prm  16928  317prm  16933  1259lem5  16942  2503lem2  16945  4001lem1  16948  4001lem2  16949  log2ub  26221  bposlem8  26561  2lgslem3d  26669  2lgsoddprmlem3d  26683  hgt750lem  33025  hgt750lem2  33026  fmtno5lem4  45448  257prm  45453  127prm  45491  gbpart7  45659  sbgoldbwt  45669  sbgoldbst  45670  ackval2012  46477
  Copyright terms: Public domain W3C validator