Theorem 4p1e5 12488

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 12408	. 2 ⊢ 5 = (4 + 1)
2	1	eqcomi 2770	1 ⊢ (4 + 1) = 5

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420  1c1 11201   + caddc 11203  4c4 12399  5c5 12400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-5 12408

This theorem is used by:  8t7e56  12939  9t6e54  12945  s5len  15051  bpoly4  16225  2exp16  17268  prmlem2  17298  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  2503lem1  17315  2503lem2  17316  2503lem3  17317  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  log2ublem3  27276  log2ub  27277  ex-exp  31051  ex-fac  31052  fib5  35037  fib6  35038  hgt750lemd  35277  hgt750lem2  35281  60gcd7e1  43055  3lexlogpow5ineq1  43104  3lexlogpow5ineq5  43110  aks4d1p1p4  43121  aks4d1p1p7  43124  aks4d1p1  43126  5bc2eq10  43192  2ap1caineq  43195  25or6to4  43256  1p4e5  43311  sq45  43682  3cubeslem3l  43696  3cubeslem3r  43697  sin5tlem4  47921  goldratmolem2  47932  fmtno1  48625  257prm  48645  fmtno4prmfac  48656  fmtno4nprmfac193  48658  fmtno5faclem2  48664  31prm  48681  127prm  48683  m11nprm  48685  ppivalnnnprm  48712  2exp340mod341  48830  nnsum3primesle9  48891  5m4e1  50934  veronesevrowd  50978  veroquadgsumlem  50982