Theorem 3p1e4 12321

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

Syntax hints:   = wceq 1542  (class class class)co 7367  1c1 11039   + caddc 11041  3c3 12237  4c4 12238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-4 12246

This theorem is referenced by:  7t6e42  12757  8t5e40  12762  9t5e45  12769  fz0to4untppr  13584  fz0to5un2tp  13585  fac4  14243  hash4  14369  hash7g  14448  s4len  14861  bpoly4  16024  2exp16  17061  43prm  17092  83prm  17093  317prm  17096  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  binom4  26814  quartlem1  26821  log2ublem3  26912  log2ub  26913  bclbnd  27243  addsqnreup  27406  tgcgr4  28599  upgr4cycl4dv4e  30255  ex-opab  30502  ex-ind-dvds  30531  evl1deg3  33638  iconstr  33910  cos9thpiminplylem1  33926  fib4  34548  fib5  34549  hgt750lem  34795  hgt750lem2  34796  3lexlogpow5ineq1  42493  3lexlogpow5ineq5  42499  aks4d1p1p5  42514  aks4d1p1  42515  1p3e4  42697  235t711  42737  3cubeslem3l  43118  3cubeslem3r  43119  inductionexd  44582  lhe4.4ex1a  44756  stoweidlem26  46454  stoweidlem34  46462  smfmullem2  47220  2ltceilhalf  47780  fmtno5lem4  48019  fmtno5  48020  fmtno5faclem2  48043  3ndvds4  48058  139prmALT  48059  31prm  48060  m5prm  48061  ppivalnnnprm  48091  11t31e341  48208  2exp340mod341  48209  8exp8mod9  48212  sbgoldbalt  48257  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  gpgprismgr4cycllem10  48580  ackval3  49159  ackval3012  49168  ackval41a  49170  ackval41  49171  ackval42  49172