Theorem 3p1e4 12362

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

Syntax hints:   = wceq 1560  (class class class)co 7396  1c1 11074   + caddc 11076  3c3 12273  4c4 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-4 12282

This theorem is referenced by:  7t6e42  12806  8t5e40  12811  9t5e45  12818  fz0to4untppr  13635  fz0to5un2tp  13636  fac4  14294  hash4  14420  hash7g  14499  s4len  14912  bpoly4  16089  2exp16  17126  43prm  17158  83prm  17159  317prm  17162  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  2503lem1  17173  2503lem2  17174  4001lem1  17177  4001lem2  17178  4001lem4  17180  4001prm  17181  binom4  26912  quartlem1  26919  log2ublem3  27010  log2ub  27011  bclbnd  27341  addsqnreup  27504  tgcgr4  28697  upgr4cycl4dv4e  30384  ex-opab  30631  ex-ind-dvds  30660  evl1deg3  33771  iconstr  34060  cos9thpiminplylem1  34076  fib4  34698  fib5  34699  hgt750lem  34942  hgt750lem2  34943  3lexlogpow5ineq1  42668  3lexlogpow5ineq5  42674  aks4d1p1p5  42689  aks4d1p1  42690  1p3e4  42871  235t711  42911  3cubeslem3l  43264  3cubeslem3r  43265  inductionexd  44728  lhe4.4ex1a  44902  stoweidlem26  46597  stoweidlem34  46605  smfmullem2  47363  2ltceilhalf  47923  fmtno5lem4  48162  fmtno5  48163  fmtno5faclem2  48186  3ndvds4  48201  139prmALT  48202  31prm  48203  m5prm  48204  ppivalnnnprm  48234  11t31e341  48351  2exp340mod341  48352  8exp8mod9  48355  sbgoldbalt  48400  sbgoldbo  48406  nnsum3primesle9  48413  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  gpgprismgr4cycllem10  48723  ackval3  49302  ackval3012  49311  ackval41a  49313  ackval41  49314  ackval42  49315