Theorem 3p1e4 12297

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

Syntax hints:   = wceq 1542  (class class class)co 7368  1c1 11039   + caddc 11041  3c3 12213  4c4 12214

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 2709

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

This theorem is referenced by:  7t6e42  12732  8t5e40  12737  9t5e45  12744  fz0to4untppr  13558  fz0to5un2tp  13559  fac4  14216  hash4  14342  hash7g  14421  s4len  14834  bpoly4  15994  2exp16  17030  43prm  17061  83prm  17062  317prm  17065  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  4001lem1  17080  4001lem2  17081  4001lem4  17083  4001prm  17084  binom4  26828  quartlem1  26835  log2ublem3  26926  log2ub  26927  bclbnd  27259  addsqnreup  27422  tgcgr4  28615  upgr4cycl4dv4e  30272  ex-opab  30519  ex-ind-dvds  30548  evl1deg3  33671  iconstr  33944  cos9thpiminplylem1  33960  fib4  34582  fib5  34583  hgt750lem  34829  hgt750lem2  34830  3lexlogpow5ineq1  42424  3lexlogpow5ineq5  42430  aks4d1p1p5  42445  aks4d1p1  42446  1p3e4  42629  235t711  42675  3cubeslem3l  43043  3cubeslem3r  43044  inductionexd  44511  lhe4.4ex1a  44685  stoweidlem26  46384  stoweidlem34  46392  smfmullem2  47150  2ltceilhalf  47688  fmtno5lem4  47916  fmtno5  47917  fmtno5faclem2  47940  3ndvds4  47955  139prmALT  47956  31prm  47957  m5prm  47958  11t31e341  48092  2exp340mod341  48093  8exp8mod9  48096  sbgoldbalt  48141  sbgoldbo  48147  nnsum3primesle9  48154  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  gpgprismgr4cycllem10  48464  ackval3  49043  ackval3012  49052  ackval41a  49054  ackval41  49055  ackval42  49056