Theorem 4p1e5 12313

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

Syntax hints:   = wceq 1547  (class class class)co 7356  1c1 11030   + caddc 11032  4c4 12229  5c5 12230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-5 12238

This theorem is referenced by:  8t7e56  12755  9t6e54  12761  s5len  14853  bpoly4  16015  2exp16  17052  prmlem2  17081  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  2503lem1  17098  2503lem2  17099  2503lem3  17100  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  log2ublem3  26930  log2ub  26931  ex-exp  30538  ex-fac  30539  fib5  34589  fib6  34590  hgt750lemd  34832  hgt750lem2  34836  60gcd7e1  42490  3lexlogpow5ineq1  42539  3lexlogpow5ineq5  42545  aks4d1p1p4  42556  aks4d1p1p7  42559  aks4d1p1  42561  5bc2eq10  42627  2ap1caineq  42630  sq45  43121  3cubeslem3l  43135  3cubeslem3r  43136  sin5tlem4  47339  goldratmolem2  47349  fmtno1  48019  257prm  48039  fmtno4prmfac  48050  fmtno4nprmfac193  48052  fmtno5faclem2  48058  31prm  48075  127prm  48077  m11nprm  48079  ppivalnnnprm  48106  2exp340mod341  48224  nnsum3primesle9  48285  5m4e1  50287