Theorem 3p1e4 12480

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7418  1c1 11194   + caddc 11196  3c3 12391  4c4 12392

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-4 12400

This theorem is used by:  7t6e42  12925  8t5e40  12930  9t5e45  12937  fz0to4untppr  13757  fz0to5un2tp  13758  fac4  14418  hash4  14544  hash7g  14624  s4len  15043  bpoly4  16218  2exp16  17261  43prm  17293  83prm  17294  317prm  17297  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  2503lem1  17308  2503lem2  17309  4001lem1  17312  4001lem2  17313  4001lem4  17315  4001prm  17316  binom4  27171  quartlem1  27178  log2ublem3  27269  log2ub  27270  bclbnd  27600  addsqnreup  27763  tgcgr4  28987  upgr4cycl4dv4e  30779  ex-opab  31026  ex-ind-dvds  31055  evl1deg3  34103  iconstr  34391  cos9thpiminplylem1  34407  fib4  35029  fib5  35030  hgt750lem  35273  hgt750lem2  35274  3lexlogpow5ineq1  43084  3lexlogpow5ineq5  43090  aks4d1p1p5  43105  aks4d1p1  43106  1p3e4  43290  235t711  43342  3cubeslem3l  43676  3cubeslem3r  43677  inductionexd  45140  lhe4.4ex1a  45298  stoweidlem26  47005  stoweidlem34  47013  smfmullem2  47771  2ltceilhalf  48371  fmtno5lem4  48610  fmtno5  48611  fmtno5faclem2  48634  3ndvds4  48649  139prmALT  48650  31prm  48651  m5prm  48652  ppivalnnnprm  48682  11t31e341  48799  2exp340mod341  48800  8exp8mod9  48803  sbgoldbalt  48848  sbgoldbo  48854  nnsum3primesle9  48861  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  gpgprismgr4cycllem10  49171  ackval3  49764  ackval3012  49773  ackval41a  49775  ackval41  49776  ackval42  49777  veronesevrowd  50948  veroquadgsumlem  50952