Theorem 4p1e5 12381

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

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   + caddc 11098  4c4 12292  5c5 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-5 12301

This theorem is referenced by:  8t7e56  12831  9t6e54  12837  s5len  14933  bpoly4  16108  2exp16  17145  prmlem2  17175  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  2503lem1  17192  2503lem2  17193  2503lem3  17194  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  log2ublem3  27113  log2ub  27114  ex-exp  30801  ex-fac  30802  fib5  34795  fib6  34796  hgt750lemd  35035  hgt750lem2  35039  60gcd7e1  42792  3lexlogpow5ineq1  42841  3lexlogpow5ineq5  42847  aks4d1p1p4  42858  aks4d1p1p7  42861  aks4d1p1  42863  5bc2eq10  42929  2ap1caineq  42932  25or6to4  42993  sq45  43423  3cubeslem3l  43437  3cubeslem3r  43438  sin5tlem4  47633  goldratmolem2  47643  fmtno1  48313  257prm  48333  fmtno4prmfac  48344  fmtno4nprmfac193  48346  fmtno5faclem2  48352  31prm  48369  127prm  48371  m11nprm  48373  ppivalnnnprm  48400  2exp340mod341  48518  nnsum3primesle9  48579  5m4e1  50637