Theorem 3p1e4 11776

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

Syntax hints:   = wceq 1533  (class class class)co 7150  1c1 10532   + caddc 10534  3c3 11687  4c4 11688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-4 11696

This theorem is referenced by:  7t6e42  12205  8t5e40  12210  9t5e45  12217  fac4  13635  hash4  13762  s4len  14255  bpoly4  15407  2exp16  16418  43prm  16449  83prm  16450  317prm  16453  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  2503lem1  16464  2503lem2  16465  4001lem1  16468  4001lem2  16469  4001lem4  16471  4001prm  16472  binom4  25422  quartlem1  25429  log2ublem3  25520  log2ub  25521  bclbnd  25850  addsqnreup  26013  tgcgr4  26311  upgr4cycl4dv4e  27958  ex-opab  28205  ex-ind-dvds  28234  fib4  31657  fib5  31658  hgt750lem  31917  hgt750lem2  31918  235t711  39170  3cubeslem3l  39276  3cubeslem3r  39277  inductionexd  40498  lhe4.4ex1a  40654  stoweidlem26  42305  stoweidlem34  42313  smfmullem2  43061  fmtno5lem4  43712  fmtno5  43713  fmtno5faclem2  43736  3ndvds4  43752  139prmALT  43753  31prm  43754  m5prm  43755  11t31e341  43891  2exp340mod341  43892  8exp8mod9  43895  sbgoldbalt  43940  sbgoldbo  43946  nnsum3primesle9  43953  nnsum4primeseven  43959  nnsum4primesevenALTV  43960