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

Theorem 4p2e6 11159
Description: 4 + 2 = 6. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
4p2e6 (4 + 2) = 6

Proof of Theorem 4p2e6
StepHypRef Expression
1 df-2 11076 . . . . 5 2 = (1 + 1)
21oveq2i 6658 . . . 4 (4 + 2) = (4 + (1 + 1))
3 4cn 11095 . . . . 5 4 ∈ ℂ
4 ax-1cn 9991 . . . . 5 1 ∈ ℂ
53, 4, 4addassi 10045 . . . 4 ((4 + 1) + 1) = (4 + (1 + 1))
62, 5eqtr4i 2646 . . 3 (4 + 2) = ((4 + 1) + 1)
7 df-5 11079 . . . 4 5 = (4 + 1)
87oveq1i 6657 . . 3 (5 + 1) = ((4 + 1) + 1)
96, 8eqtr4i 2646 . 2 (4 + 2) = (5 + 1)
10 df-6 11080 . 2 6 = (5 + 1)
119, 10eqtr4i 2646 1 (4 + 2) = 6
Colors of variables: wff setvar class
Syntax hints:   = wceq 1482  (class class class)co 6647  1c1 9934   + caddc 9936  2c2 11067  4c4 11069  5c5 11070  6c6 11071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-addass 9998  ax-i2m1 10001  ax-1ne0 10002  ax-rrecex 10005  ax-cnre 10006
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-iota 5849  df-fv 5894  df-ov 6650  df-2 11076  df-3 11077  df-4 11078  df-5 11079  df-6 11080
This theorem is referenced by:  4p3e7  11160  div4p1lem1div2  11284  4t4e16  11630  6gcd4e2  15249  2exp16  15791  163prm  15826  631prm  15828  1259lem4  15835  2503lem2  15839  2503lem3  15840  4001lem1  15842  4001lem2  15843  4001lem4  15845  bposlem9  25011  hgt750lem2  30715  lhe4.4ex1a  38354  fmtno4prmfac  41255  fmtno5faclem1  41262  gbowgt5  41421  mogoldbb  41444
  Copyright terms: Public domain W3C validator