Theorem 4p1e5 11154

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

Syntax hints:   = wceq 1483  (class class class)co 6650  1c1 9937   + caddc 9939  4c4 11072  5c5 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-5 11082

This theorem is referenced by:  8t7e56  11661  9t6e54  11667  s5len  13645  bpoly4  14790  2exp16  15797  prmlem2  15827  163prm  15832  317prm  15833  631prm  15834  prmo5  15836  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  2503lem1  15844  2503lem2  15845  2503lem3  15846  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  log2ublem3  24675  log2ub  24676  ex-exp  27307  ex-fac  27308  fib5  30467  fib6  30468  hgt750lemd  30726  hgt750lem2  30730  fmtno1  41453  257prm  41473  fmtno4prmfac  41484  fmtno4nprmfac193  41486  fmtno5faclem2  41492  31prm  41512  127prm  41515  m11nprm  41518  nnsum3primesle9  41682  5m4e1  42543