Theorem 4p1e5 12334

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  4c4 12250  5c5 12251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-5 12259

This theorem is referenced by:  8t7e56  12776  9t6e54  12782  s5len  14873  bpoly4  16032  2exp16  17068  prmlem2  17097  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  log2ublem3  26865  log2ub  26866  ex-exp  30386  ex-fac  30387  fib5  34403  fib6  34404  hgt750lemd  34646  hgt750lem2  34650  60gcd7e1  42000  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p1  42071  5bc2eq10  42137  2ap1caineq  42140  sq45  42666  3cubeslem3l  42681  3cubeslem3r  42682  fmtno1  47546  257prm  47566  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno5faclem2  47585  31prm  47602  127prm  47604  m11nprm  47606  2exp340mod341  47738  nnsum3primesle9  47799  5m4e1  49790