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

Theorem 4p3e7 11989
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 11899 . . . 4 3 = (2 + 1)
21oveq2i 7229 . . 3 (4 + 3) = (4 + (2 + 1))
3 4cn 11920 . . . 4 4 ∈ ℂ
4 2cn 11910 . . . 4 2 ∈ ℂ
5 ax-1cn 10792 . . . 4 1 ∈ ℂ
63, 4, 5addassi 10848 . . 3 ((4 + 2) + 1) = (4 + (2 + 1))
72, 6eqtr4i 2768 . 2 (4 + 3) = ((4 + 2) + 1)
8 df-7 11903 . . 3 7 = (6 + 1)
9 4p2e6 11988 . . . 4 (4 + 2) = 6
109oveq1i 7228 . . 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 1543  (class class class)co 7218  1c1 10735   + caddc 10737  2c2 11890  3c3 11891  4c4 11892  6c6 11894  7c7 11895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-1cn 10792  ax-addcl 10794  ax-addass 10799
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3415  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-br 5059  df-iota 6343  df-fv 6393  df-ov 7221  df-2 11898  df-3 11899  df-4 11900  df-5 11901  df-6 11902  df-7 11903
This theorem is referenced by:  4p4e8  11990  37prm  16679  317prm  16684  1259lem5  16693  2503lem2  16696  4001lem1  16699  4001lem2  16700  log2ub  25837  bposlem8  26177  2lgslem3d  26285  2lgsoddprmlem3d  26299  hgt750lem  32348  hgt750lem2  32349  fmtno5lem4  44689  257prm  44694  127prm  44732  gbpart7  44900  sbgoldbwt  44910  sbgoldbst  44911  ackval2012  45718
  Copyright terms: Public domain W3C validator