Theorem 4p1e5 12303

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  4c4 12219  5c5 12220

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 12228

This theorem is referenced by:  8t7e56  12745  9t6e54  12751  s5len  14842  bpoly4  16001  2exp16  17037  prmlem2  17066  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  2503lem1  17083  2503lem2  17084  2503lem3  17085  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  log2ublem3  26891  log2ub  26892  ex-exp  30429  ex-fac  30430  fib5  34389  fib6  34390  hgt750lemd  34632  hgt750lem2  34636  60gcd7e1  41986  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1  42057  5bc2eq10  42123  2ap1caineq  42126  sq45  42652  3cubeslem3l  42667  3cubeslem3r  42668  fmtno1  47535  257prm  47555  fmtno4prmfac  47566  fmtno4nprmfac193  47568  fmtno5faclem2  47574  31prm  47591  127prm  47593  m11nprm  47595  2exp340mod341  47727  nnsum3primesle9  47788  5m4e1  49779