Theorem 3p1e4 12265

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

Syntax hints:   = wceq 1541  (class class class)co 7346  1c1 11007   + caddc 11009  3c3 12181  4c4 12182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-4 12190

This theorem is referenced by:  7t6e42  12701  8t5e40  12706  9t5e45  12713  fz0to4untppr  13530  fz0to5un2tp  13531  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  26787  quartlem1  26794  log2ublem3  26885  log2ub  26886  bclbnd  27218  addsqnreup  27381  tgcgr4  28509  upgr4cycl4dv4e  30165  ex-opab  30412  ex-ind-dvds  30441  evl1deg3  33541  iconstr  33779  cos9thpiminplylem1  33795  fib4  34417  fib5  34418  hgt750lem  34664  hgt750lem2  34665  3lexlogpow5ineq1  42095  3lexlogpow5ineq5  42101  aks4d1p1p5  42116  aks4d1p1  42117  1p3e4  42300  235t711  42346  3cubeslem3l  42727  3cubeslem3r  42728  inductionexd  44196  lhe4.4ex1a  44370  stoweidlem26  46072  stoweidlem34  46080  smfmullem2  46838  2ltceilhalf  47367  fmtno5lem4  47595  fmtno5  47596  fmtno5faclem2  47619  3ndvds4  47634  139prmALT  47635  31prm  47636  m5prm  47637  11t31e341  47771  2exp340mod341  47772  8exp8mod9  47775  sbgoldbalt  47820  sbgoldbo  47826  nnsum3primesle9  47833  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  gpgprismgr4cycllem10  48143  ackval3  48723  ackval3012  48732  ackval41a  48734  ackval41  48735  ackval42  48736