Theorem 4p1e5 12266

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  4c4 12182  5c5 12183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-5 12191

This theorem is referenced by:  8t7e56  12708  9t6e54  12714  s5len  14807  bpoly4  15966  2exp16  17002  prmlem2  17031  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  2503lem1  17048  2503lem2  17049  2503lem3  17050  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  log2ublem3  26885  log2ub  26886  ex-exp  30430  ex-fac  30431  fib5  34418  fib6  34419  hgt750lemd  34661  hgt750lem2  34665  60gcd7e1  42108  3lexlogpow5ineq1  42157  3lexlogpow5ineq5  42163  aks4d1p1p4  42174  aks4d1p1p7  42177  aks4d1p1  42179  5bc2eq10  42245  2ap1caineq  42248  sq45  42774  3cubeslem3l  42789  3cubeslem3r  42790  fmtno1  47651  257prm  47671  fmtno4prmfac  47682  fmtno4nprmfac193  47684  fmtno5faclem2  47690  31prm  47707  127prm  47709  m11nprm  47711  2exp340mod341  47843  nnsum3primesle9  47904  5m4e1  49908