Theorem 4p1e5 12391

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

Syntax hints:   = wceq 1540  (class class class)co 7410  1c1 11135   + caddc 11137  4c4 12302  5c5 12303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-5 12311

This theorem is referenced by:  8t7e56  12833  9t6e54  12839  s5len  14924  bpoly4  16080  2exp16  17115  prmlem2  17144  163prm  17149  317prm  17150  631prm  17151  1259lem1  17155  1259lem2  17156  1259lem3  17157  1259lem4  17158  2503lem1  17161  2503lem2  17162  2503lem3  17163  4001lem1  17165  4001lem2  17166  4001lem3  17167  4001lem4  17168  log2ublem3  26915  log2ub  26916  ex-exp  30436  ex-fac  30437  fib5  34442  fib6  34443  hgt750lemd  34685  hgt750lem2  34689  60gcd7e1  42023  3lexlogpow5ineq1  42072  3lexlogpow5ineq5  42078  aks4d1p1p4  42089  aks4d1p1p7  42092  aks4d1p1  42094  5bc2eq10  42160  2ap1caineq  42163  sq45  42661  3cubeslem3l  42676  3cubeslem3r  42677  fmtno1  47522  257prm  47542  fmtno4prmfac  47553  fmtno4nprmfac193  47555  fmtno5faclem2  47561  31prm  47578  127prm  47580  m11nprm  47582  2exp340mod341  47714  nnsum3primesle9  47775  5m4e1  49628