Theorem 3p1e4 12315

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

Syntax hints:   = wceq 1542  (class class class)co 7361  1c1 11033   + caddc 11035  3c3 12231  4c4 12232

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 12240

This theorem is referenced by:  7t6e42  12751  8t5e40  12756  9t5e45  12763  fz0to4untppr  13578  fz0to5un2tp  13579  fac4  14237  hash4  14363  hash7g  14442  s4len  14855  bpoly4  16018  2exp16  17055  43prm  17086  83prm  17087  317prm  17090  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  2503lem1  17101  2503lem2  17102  4001lem1  17105  4001lem2  17106  4001lem4  17108  4001prm  17109  binom4  26830  quartlem1  26837  log2ublem3  26928  log2ub  26929  bclbnd  27260  addsqnreup  27423  tgcgr4  28616  upgr4cycl4dv4e  30273  ex-opab  30520  ex-ind-dvds  30549  evl1deg3  33656  iconstr  33929  cos9thpiminplylem1  33945  fib4  34567  fib5  34568  hgt750lem  34814  hgt750lem2  34815  3lexlogpow5ineq1  42510  3lexlogpow5ineq5  42516  aks4d1p1p5  42531  aks4d1p1  42532  1p3e4  42714  235t711  42754  3cubeslem3l  43135  3cubeslem3r  43136  inductionexd  44603  lhe4.4ex1a  44777  stoweidlem26  46475  stoweidlem34  46483  smfmullem2  47241  2ltceilhalf  47795  fmtno5lem4  48034  fmtno5  48035  fmtno5faclem2  48058  3ndvds4  48073  139prmALT  48074  31prm  48075  m5prm  48076  ppivalnnnprm  48106  11t31e341  48223  2exp340mod341  48224  8exp8mod9  48227  sbgoldbalt  48272  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  gpgprismgr4cycllem10  48595  ackval3  49174  ackval3012  49183  ackval41a  49185  ackval41  49186  ackval42  49187