Theorem 3p1e4 12400

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419  1c1 11116   + caddc 11118  3c3 12311  4c4 12312

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 2156  ax-ext 2737

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

This theorem is used by:  7t6e42  12845  8t5e40  12850  9t5e45  12857  fz0to4untppr  13675  fz0to5un2tp  13676  fac4  14335  hash4  14461  hash7g  14541  s4len  14960  bpoly4  16135  2exp16  17172  43prm  17204  83prm  17205  317prm  17208  1259lem2  17214  1259lem3  17215  1259lem4  17216  1259lem5  17217  2503lem1  17219  2503lem2  17220  4001lem1  17223  4001lem2  17224  4001lem4  17226  4001prm  17227  binom4  27066  quartlem1  27073  log2ublem3  27164  log2ub  27165  bclbnd  27495  addsqnreup  27658  tgcgr4  28851  upgr4cycl4dv4e  30607  ex-opab  30854  ex-ind-dvds  30883  evl1deg3  33932  iconstr  34220  cos9thpiminplylem1  34236  fib4  34859  fib5  34860  hgt750lem  35103  hgt750lem2  35104  3lexlogpow5ineq1  42879  3lexlogpow5ineq5  42885  aks4d1p1p5  42900  aks4d1p1  42901  1p3e4  43084  235t711  43124  3cubeslem3l  43475  3cubeslem3r  43476  inductionexd  44939  lhe4.4ex1a  45097  stoweidlem26  46798  stoweidlem34  46806  smfmullem2  47564  2ltceilhalf  48127  fmtno5lem4  48366  fmtno5  48367  fmtno5faclem2  48390  3ndvds4  48405  139prmALT  48406  31prm  48407  m5prm  48408  ppivalnnnprm  48438  11t31e341  48555  2exp340mod341  48556  8exp8mod9  48559  sbgoldbalt  48604  sbgoldbo  48610  nnsum3primesle9  48617  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  gpgprismgr4cycllem10  48927  ackval3  49520  ackval3012  49529  ackval41a  49531  ackval41  49532  ackval42  49533