Theorem 4p1e5 12358

Description: 4 + 1 = 5. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
4p1e5	⊢ (4 + 1) = 5

Proof of Theorem 4p1e5

Step	Hyp	Ref	Expression
1		df-5 12278	. 2 ⊢ 5 = (4 + 1)
2	1	eqcomi 2742	1 ⊢ (4 + 1) = 5

Syntax hints:   = wceq 1542  (class class class)co 7409  1c1 11111   + caddc 11113  4c4 12269  5c5 12270

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-5 12278

This theorem is referenced by:  8t7e56  12797  9t6e54  12803  s5len  14851  bpoly4  16003  2exp16  17024  prmlem2  17053  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  2503lem1  17070  2503lem2  17071  2503lem3  17072  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  log2ublem3  26453  log2ub  26454  ex-exp  29703  ex-fac  29704  fib5  33404  fib6  33405  hgt750lemd  33660  hgt750lem2  33664  60gcd7e1  40870  3lexlogpow5ineq1  40919  3lexlogpow5ineq5  40925  aks4d1p1p4  40936  aks4d1p1p7  40939  aks4d1p1  40941  5bc2eq10  40958  2ap1caineq  40961  sq45  41413  3cubeslem3l  41424  3cubeslem3r  41425  fmtno1  46209  257prm  46229  fmtno4prmfac  46240  fmtno4nprmfac193  46242  fmtno5faclem2  46248  31prm  46265  127prm  46267  m11nprm  46269  2exp340mod341  46401  nnsum3primesle9  46462  5m4e1  47844