Theorem 3p1e4 12383

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

Syntax hints:   = wceq 1540  (class class class)co 7403  1c1 11128   + caddc 11130  3c3 12294  4c4 12295

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  7t6e42  12819  8t5e40  12824  9t5e45  12831  fz0to4untppr  13645  fz0to5un2tp  13646  fac4  14297  hash4  14423  hash7g  14502  s4len  14916  bpoly4  16073  2exp16  17108  43prm  17139  83prm  17140  317prm  17143  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  4001lem1  17158  4001lem2  17159  4001lem4  17161  4001prm  17162  binom4  26810  quartlem1  26817  log2ublem3  26908  log2ub  26909  bclbnd  27241  addsqnreup  27404  tgcgr4  28456  upgr4cycl4dv4e  30112  ex-opab  30359  ex-ind-dvds  30388  evl1deg3  33537  iconstr  33746  cos9thpiminplylem1  33762  fib4  34382  fib5  34383  hgt750lem  34629  hgt750lem2  34630  3lexlogpow5ineq1  42013  3lexlogpow5ineq5  42019  aks4d1p1p5  42034  aks4d1p1  42035  235t711  42301  3cubeslem3l  42656  3cubeslem3r  42657  inductionexd  44126  lhe4.4ex1a  44301  stoweidlem26  46003  stoweidlem34  46011  smfmullem2  46769  2ltceilhalf  47305  fmtno5lem4  47518  fmtno5  47519  fmtno5faclem2  47542  3ndvds4  47557  139prmALT  47558  31prm  47559  m5prm  47560  11t31e341  47694  2exp340mod341  47695  8exp8mod9  47698  sbgoldbalt  47743  sbgoldbo  47749  nnsum3primesle9  47756  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  gpgprismgr4cycllem10  48051  ackval3  48611  ackval3012  48620  ackval41a  48622  ackval41  48623  ackval42  48624