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  26834  log2ub  26835  ex-exp  30352  ex-fac  30353  fib5  34369  fib6  34370  hgt750lemd  34612  hgt750lem2  34616  60gcd7e1  41966  3lexlogpow5ineq1  42015  3lexlogpow5ineq5  42021  aks4d1p1p4  42032  aks4d1p1p7  42035  aks4d1p1  42037  5bc2eq10  42103  2ap1caineq  42106  sq45  42632  3cubeslem3l  42647  3cubeslem3r  42648  fmtno1  47515  257prm  47535  fmtno4prmfac  47546  fmtno4nprmfac193  47548  fmtno5faclem2  47554  31prm  47571  127prm  47573  m11nprm  47575  2exp340mod341  47707  nnsum3primesle9  47768  5m4e1  49759