Theorem 4p1e5 12327

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  4c4 12243  5c5 12244

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 2701

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

This theorem is referenced by:  8t7e56  12769  9t6e54  12775  s5len  14866  bpoly4  16025  2exp16  17061  prmlem2  17090  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  2503lem1  17107  2503lem2  17108  2503lem3  17109  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  log2ublem3  26858  log2ub  26859  ex-exp  30379  ex-fac  30380  fib5  34396  fib6  34397  hgt750lemd  34639  hgt750lem2  34643  60gcd7e1  41993  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p1  42064  5bc2eq10  42130  2ap1caineq  42133  sq45  42659  3cubeslem3l  42674  3cubeslem3r  42675  fmtno1  47542  257prm  47562  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno5faclem2  47581  31prm  47598  127prm  47600  m11nprm  47602  2exp340mod341  47734  nnsum3primesle9  47795  5m4e1  49786