Theorem 4p1e5 12269

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  4c4 12185  5c5 12186

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 2701

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

This theorem is referenced by:  8t7e56  12711  9t6e54  12717  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  26856  log2ub  26857  ex-exp  30394  ex-fac  30395  fib5  34373  fib6  34374  hgt750lemd  34616  hgt750lem2  34620  60gcd7e1  41982  3lexlogpow5ineq1  42031  3lexlogpow5ineq5  42037  aks4d1p1p4  42048  aks4d1p1p7  42051  aks4d1p1  42053  5bc2eq10  42119  2ap1caineq  42122  sq45  42648  3cubeslem3l  42663  3cubeslem3r  42664  fmtno1  47529  257prm  47549  fmtno4prmfac  47560  fmtno4nprmfac193  47562  fmtno5faclem2  47568  31prm  47585  127prm  47587  m11nprm  47589  2exp340mod341  47721  nnsum3primesle9  47782  5m4e1  49786