Theorem 3p1e4 12364

Description: 3 + 1 = 4. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
3p1e4	⊢ (3 + 1) = 4

Proof of Theorem 3p1e4

Step	Hyp	Ref	Expression
1		df-4 12284	. 2 ⊢ 4 = (3 + 1)
2	1	eqcomi 2740	1 ⊢ (3 + 1) = 4

Syntax hints:   = wceq 1540  (class class class)co 7412  1c1 11117   + caddc 11119  3c3 12275  4c4 12276

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-4 12284

This theorem is referenced by:  7t6e42  12797  8t5e40  12802  9t5e45  12809  fac4  14248  hash4  14374  s4len  14857  bpoly4  16010  2exp16  17031  43prm  17062  83prm  17063  317prm  17066  1259lem2  17072  1259lem3  17073  1259lem4  17074  1259lem5  17075  2503lem1  17077  2503lem2  17078  4001lem1  17081  4001lem2  17082  4001lem4  17084  4001prm  17085  binom4  26696  quartlem1  26703  log2ublem3  26794  log2ub  26795  bclbnd  27126  addsqnreup  27289  tgcgr4  28215  upgr4cycl4dv4e  29871  ex-opab  30118  ex-ind-dvds  30147  fib4  33867  fib5  33868  hgt750lem  34127  hgt750lem2  34128  3lexlogpow5ineq1  41386  3lexlogpow5ineq5  41392  aks4d1p1p5  41407  aks4d1p1  41408  235t711  41668  3cubeslem3l  41887  3cubeslem3r  41888  inductionexd  43369  lhe4.4ex1a  43551  stoweidlem26  45201  stoweidlem34  45209  smfmullem2  45967  fmtno5lem4  46683  fmtno5  46684  fmtno5faclem2  46707  3ndvds4  46722  139prmALT  46723  31prm  46724  m5prm  46725  11t31e341  46859  2exp340mod341  46860  8exp8mod9  46863  sbgoldbalt  46908  sbgoldbo  46914  nnsum3primesle9  46921  nnsum4primeseven  46927  nnsum4primesevenALTV  46928  ackval3  47531  ackval3012  47540  ackval41a  47542  ackval41  47543  ackval42  47544