Theorem 3p1e4 12268

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

Syntax hints:   = wceq 1540  (class class class)co 7349  1c1 11010   + caddc 11012  3c3 12184  4c4 12185

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-4 12193

This theorem is referenced by:  7t6e42  12704  8t5e40  12709  9t5e45  12716  fz0to4untppr  13533  fz0to5un2tp  13534  fac4  14188  hash4  14314  hash7g  14393  s4len  14806  bpoly4  15966  2exp16  17002  43prm  17033  83prm  17034  317prm  17037  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  4001lem1  17052  4001lem2  17053  4001lem4  17055  4001prm  17056  binom4  26758  quartlem1  26765  log2ublem3  26856  log2ub  26857  bclbnd  27189  addsqnreup  27352  tgcgr4  28480  upgr4cycl4dv4e  30133  ex-opab  30380  ex-ind-dvds  30409  evl1deg3  33522  iconstr  33749  cos9thpiminplylem1  33765  fib4  34388  fib5  34389  hgt750lem  34635  hgt750lem2  34636  3lexlogpow5ineq1  42047  3lexlogpow5ineq5  42053  aks4d1p1p5  42068  aks4d1p1  42069  1p3e4  42252  235t711  42298  3cubeslem3l  42679  3cubeslem3r  42680  inductionexd  44148  lhe4.4ex1a  44322  stoweidlem26  46027  stoweidlem34  46035  smfmullem2  46793  2ltceilhalf  47332  fmtno5lem4  47560  fmtno5  47561  fmtno5faclem2  47584  3ndvds4  47599  139prmALT  47600  31prm  47601  m5prm  47602  11t31e341  47736  2exp340mod341  47737  8exp8mod9  47740  sbgoldbalt  47785  sbgoldbo  47791  nnsum3primesle9  47798  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  gpgprismgr4cycllem10  48108  ackval3  48688  ackval3012  48697  ackval41a  48699  ackval41  48700  ackval42  48701