Theorem 4p1e5 12403

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11118   + caddc 11120  4c4 12314  5c5 12315

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-5 12323

This theorem is used by:  8t7e56  12854  9t6e54  12860  s5len  14963  bpoly4  16137  2exp16  17174  prmlem2  17204  163prm  17209  317prm  17210  631prm  17211  1259lem1  17215  1259lem2  17216  1259lem3  17217  1259lem4  17218  2503lem1  17221  2503lem2  17222  2503lem3  17223  4001lem1  17225  4001lem2  17226  4001lem3  17227  4001lem4  17228  log2ublem3  27166  log2ub  27167  ex-exp  30874  ex-fac  30875  fib5  34862  fib6  34863  hgt750lemd  35102  hgt750lem2  35106  60gcd7e1  42832  3lexlogpow5ineq1  42881  3lexlogpow5ineq5  42887  aks4d1p1p4  42898  aks4d1p1p7  42901  aks4d1p1  42903  5bc2eq10  42969  2ap1caineq  42972  25or6to4  43033  sq45  43463  3cubeslem3l  43477  3cubeslem3r  43478  sin5tlem4  47673  goldratmolem2  47683  fmtno1  48353  257prm  48373  fmtno4prmfac  48384  fmtno4nprmfac193  48386  fmtno5faclem2  48392  31prm  48409  127prm  48411  m11nprm  48413  ppivalnnnprm  48440  2exp340mod341  48558  nnsum3primesle9  48619  5m4e1  50676