Theorem 4p1e5 12385

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11100   + caddc 11102  4c4 12296  5c5 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-5 12305

This theorem is referenced by:  8t7e56  12835  9t6e54  12841  s5len  14936  bpoly4  16112  2exp16  17149  prmlem2  17179  163prm  17184  317prm  17185  631prm  17186  1259lem1  17190  1259lem2  17191  1259lem3  17192  1259lem4  17193  2503lem1  17196  2503lem2  17197  2503lem3  17198  4001lem1  17200  4001lem2  17201  4001lem3  17202  4001lem4  17203  log2ublem3  27078  log2ub  27079  ex-exp  30741  ex-fac  30742  fib5  34739  fib6  34740  hgt750lemd  34979  hgt750lem2  34983  60gcd7e1  42661  3lexlogpow5ineq1  42710  3lexlogpow5ineq5  42716  aks4d1p1p4  42727  aks4d1p1p7  42730  aks4d1p1  42732  5bc2eq10  42798  2ap1caineq  42801  25or6to4  42862  sq45  43294  3cubeslem3l  43308  3cubeslem3r  43309  sin5tlem4  47501  goldratmolem2  47511  fmtno1  48181  257prm  48201  fmtno4prmfac  48212  fmtno4nprmfac193  48214  fmtno5faclem2  48220  31prm  48237  127prm  48239  m11nprm  48241  ppivalnnnprm  48268  2exp340mod341  48386  nnsum3primesle9  48447  5m4e1  50470