Theorem 3p1e4 12283

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

Syntax hints:   = wceq 1541  (class class class)co 7356  1c1 11025   + caddc 11027  3c3 12199  4c4 12200

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 2123  ax-ext 2706

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

This theorem is referenced by:  7t6e42  12718  8t5e40  12723  9t5e45  12730  fz0to4untppr  13544  fz0to5un2tp  13545  fac4  14202  hash4  14328  hash7g  14407  s4len  14820  bpoly4  15980  2exp16  17016  43prm  17047  83prm  17048  317prm  17051  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  4001lem1  17066  4001lem2  17067  4001lem4  17069  4001prm  17070  binom4  26814  quartlem1  26821  log2ublem3  26912  log2ub  26913  bclbnd  27245  addsqnreup  27408  tgcgr4  28552  upgr4cycl4dv4e  30209  ex-opab  30456  ex-ind-dvds  30485  evl1deg3  33608  iconstr  33872  cos9thpiminplylem1  33888  fib4  34510  fib5  34511  hgt750lem  34757  hgt750lem2  34758  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1p5  42268  aks4d1p1  42269  1p3e4  42456  235t711  42502  3cubeslem3l  42870  3cubeslem3r  42871  inductionexd  44338  lhe4.4ex1a  44512  stoweidlem26  46212  stoweidlem34  46220  smfmullem2  46978  2ltceilhalf  47516  fmtno5lem4  47744  fmtno5  47745  fmtno5faclem2  47768  3ndvds4  47783  139prmALT  47784  31prm  47785  m5prm  47786  11t31e341  47920  2exp340mod341  47921  8exp8mod9  47924  sbgoldbalt  47969  sbgoldbo  47975  nnsum3primesle9  47982  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  gpgprismgr4cycllem10  48292  ackval3  48871  ackval3012  48880  ackval41a  48882  ackval41  48883  ackval42  48884