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

Theorem 4p1e5 12300
Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)
Assertion
Ref Expression
4p1e5 (4 + 1) = 5

Proof of Theorem 4p1e5
StepHypRef Expression
1 df-5 12220 . 2 5 = (4 + 1)
21eqcomi 2746 1 (4 + 1) = 5
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7358  1c1 11053   + caddc 11055  4c4 12211  5c5 12212
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-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-5 12220
This theorem is referenced by:  8t7e56  12739  9t6e54  12745  s5len  14790  bpoly4  15943  2exp16  16964  prmlem2  16993  163prm  16998  317prm  16999  631prm  17000  1259lem1  17004  1259lem2  17005  1259lem3  17006  1259lem4  17007  2503lem1  17010  2503lem2  17011  2503lem3  17012  4001lem1  17014  4001lem2  17015  4001lem3  17016  4001lem4  17017  log2ublem3  26301  log2ub  26302  ex-exp  29397  ex-fac  29398  fib5  33008  fib6  33009  hgt750lemd  33264  hgt750lem2  33268  60gcd7e1  40465  3lexlogpow5ineq1  40514  3lexlogpow5ineq5  40520  aks4d1p1p4  40531  aks4d1p1p7  40534  aks4d1p1  40536  5bc2eq10  40553  2ap1caineq  40556  3cubeslem3l  41012  3cubeslem3r  41013  fmtno1  45740  257prm  45760  fmtno4prmfac  45771  fmtno4nprmfac193  45773  fmtno5faclem2  45779  31prm  45796  127prm  45798  m11nprm  45800  2exp340mod341  45932  nnsum3primesle9  45993  5m4e1  47251
  Copyright terms: Public domain W3C validator