Theorem 3p1e4 12333

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 12258	. 2 ⊢ 4 = (3 + 1)
2	1	eqcomi 2739	1 ⊢ (3 + 1) = 4

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   + caddc 11078  3c3 12249  4c4 12250

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-4 12258

This theorem is referenced by:  7t6e42  12769  8t5e40  12774  9t5e45  12781  fz0to4untppr  13598  fz0to5un2tp  13599  fac4  14253  hash4  14379  hash7g  14458  s4len  14872  bpoly4  16032  2exp16  17068  43prm  17099  83prm  17100  317prm  17103  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  4001lem1  17118  4001lem2  17119  4001lem4  17121  4001prm  17122  binom4  26767  quartlem1  26774  log2ublem3  26865  log2ub  26866  bclbnd  27198  addsqnreup  27361  tgcgr4  28465  upgr4cycl4dv4e  30121  ex-opab  30368  ex-ind-dvds  30397  evl1deg3  33554  iconstr  33763  cos9thpiminplylem1  33779  fib4  34402  fib5  34403  hgt750lem  34649  hgt750lem2  34650  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p5  42070  aks4d1p1  42071  1p3e4  42254  235t711  42300  3cubeslem3l  42681  3cubeslem3r  42682  inductionexd  44151  lhe4.4ex1a  44325  stoweidlem26  46031  stoweidlem34  46039  smfmullem2  46797  2ltceilhalf  47333  fmtno5lem4  47561  fmtno5  47562  fmtno5faclem2  47585  3ndvds4  47600  139prmALT  47601  31prm  47602  m5prm  47603  11t31e341  47737  2exp340mod341  47738  8exp8mod9  47741  sbgoldbalt  47786  sbgoldbo  47792  nnsum3primesle9  47799  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  gpgprismgr4cycllem10  48098  ackval3  48676  ackval3012  48685  ackval41a  48687  ackval41  48688  ackval42  48689