Theorem 3p1e4 12285

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

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11027   + caddc 11029  3c3 12201  4c4 12202

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 2708

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

This theorem is referenced by:  7t6e42  12720  8t5e40  12725  9t5e45  12732  fz0to4untppr  13546  fz0to5un2tp  13547  fac4  14204  hash4  14330  hash7g  14409  s4len  14822  bpoly4  15982  2exp16  17018  43prm  17049  83prm  17050  317prm  17053  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  2503lem1  17064  2503lem2  17065  4001lem1  17068  4001lem2  17069  4001lem4  17071  4001prm  17072  binom4  26816  quartlem1  26823  log2ublem3  26914  log2ub  26915  bclbnd  27247  addsqnreup  27410  tgcgr4  28603  upgr4cycl4dv4e  30260  ex-opab  30507  ex-ind-dvds  30536  evl1deg3  33659  iconstr  33923  cos9thpiminplylem1  33939  fib4  34561  fib5  34562  hgt750lem  34808  hgt750lem2  34809  3lexlogpow5ineq1  42308  3lexlogpow5ineq5  42314  aks4d1p1p5  42329  aks4d1p1  42330  1p3e4  42514  235t711  42560  3cubeslem3l  42928  3cubeslem3r  42929  inductionexd  44396  lhe4.4ex1a  44570  stoweidlem26  46270  stoweidlem34  46278  smfmullem2  47036  2ltceilhalf  47574  fmtno5lem4  47802  fmtno5  47803  fmtno5faclem2  47826  3ndvds4  47841  139prmALT  47842  31prm  47843  m5prm  47844  11t31e341  47978  2exp340mod341  47979  8exp8mod9  47982  sbgoldbalt  48027  sbgoldbo  48033  nnsum3primesle9  48040  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  gpgprismgr4cycllem10  48350  ackval3  48929  ackval3012  48938  ackval41a  48940  ackval41  48941  ackval42  48942