Theorem 3p1e4 12408

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

Syntax hints:   = wceq 1536  (class class class)co 7430  1c1 11153   + caddc 11155  3c3 12319  4c4 12320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-4 12328

This theorem is referenced by:  7t6e42  12843  8t5e40  12848  9t5e45  12855  fz0to4untppr  13666  fz0to5un2tp  13667  fac4  14316  hash4  14442  hash7g  14521  s4len  14934  bpoly4  16091  2exp16  17124  43prm  17155  83prm  17156  317prm  17159  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  2503lem1  17170  2503lem2  17171  4001lem1  17174  4001lem2  17175  4001lem4  17177  4001prm  17178  binom4  26907  quartlem1  26914  log2ublem3  27005  log2ub  27006  bclbnd  27338  addsqnreup  27501  tgcgr4  28553  upgr4cycl4dv4e  30213  ex-opab  30460  ex-ind-dvds  30489  evl1deg3  33582  fib4  34385  fib5  34386  hgt750lem  34644  hgt750lem2  34645  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p5  42056  aks4d1p1  42057  235t711  42317  3cubeslem3l  42673  3cubeslem3r  42674  inductionexd  44144  lhe4.4ex1a  44324  stoweidlem26  45981  stoweidlem34  45989  smfmullem2  46747  fmtno5lem4  47480  fmtno5  47481  fmtno5faclem2  47504  3ndvds4  47519  139prmALT  47520  31prm  47521  m5prm  47522  11t31e341  47656  2exp340mod341  47657  8exp8mod9  47660  sbgoldbalt  47705  sbgoldbo  47711  nnsum3primesle9  47718  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  2ltceilhalf  47949  ackval3  48532  ackval3012  48541  ackval41a  48543  ackval41  48544  ackval42  48545