Theorem 4p1e5 12439

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  4c4 12350  5c5 12351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-5 12359

This theorem is referenced by:  8t7e56  12878  9t6e54  12884  s5len  14949  bpoly4  16107  2exp16  17138  prmlem2  17167  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  log2ublem3  27009  log2ub  27010  ex-exp  30482  ex-fac  30483  fib5  34370  fib6  34371  hgt750lemd  34625  hgt750lem2  34629  60gcd7e1  41962  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p1  42033  5bc2eq10  42099  2ap1caineq  42102  sq45  42626  3cubeslem3l  42642  3cubeslem3r  42643  fmtno1  47415  257prm  47435  fmtno4prmfac  47446  fmtno4nprmfac193  47448  fmtno5faclem2  47454  31prm  47471  127prm  47473  m11nprm  47475  2exp340mod341  47607  nnsum3primesle9  47668  5m4e1  48891