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  28476  upgr4cycl4dv4e  30129  ex-opab  30376  ex-ind-dvds  30405  evl1deg3  33513  iconstr  33733  cos9thpiminplylem1  33749  fib4  34372  fib5  34373  hgt750lem  34619  hgt750lem2  34620  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  aks4d1p1p5  42048  aks4d1p1  42049  1p3e4  42232  235t711  42278  3cubeslem3l  42659  3cubeslem3r  42660  inductionexd  44128  lhe4.4ex1a  44302  stoweidlem26  46007  stoweidlem34  46015  smfmullem2  46773  2ltceilhalf  47312  fmtno5lem4  47540  fmtno5  47541  fmtno5faclem2  47564  3ndvds4  47579  139prmALT  47580  31prm  47581  m5prm  47582  11t31e341  47716  2exp340mod341  47717  8exp8mod9  47720  sbgoldbalt  47765  sbgoldbo  47771  nnsum3primesle9  47778  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  gpgprismgr4cycllem10  48088  ackval3  48668  ackval3012  48677  ackval41a  48679  ackval41  48680  ackval42  48681