Theorem 3p1e4 11770

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

Syntax hints:   = wceq 1538  (class class class)co 7135  1c1 10527   + caddc 10529  3c3 11681  4c4 11682

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-4 11690

This theorem is referenced by:  7t6e42  12199  8t5e40  12204  9t5e45  12211  fac4  13637  hash4  13764  s4len  14252  bpoly4  15405  2exp16  16416  43prm  16447  83prm  16448  317prm  16451  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  4001lem1  16466  4001lem2  16467  4001lem4  16469  4001prm  16470  binom4  25436  quartlem1  25443  log2ublem3  25534  log2ub  25535  bclbnd  25864  addsqnreup  26027  tgcgr4  26325  upgr4cycl4dv4e  27970  ex-opab  28217  ex-ind-dvds  28246  fib4  31772  fib5  31773  hgt750lem  32032  hgt750lem2  32033  235t711  39485  3cubeslem3l  39627  3cubeslem3r  39628  inductionexd  40858  lhe4.4ex1a  41033  stoweidlem26  42668  stoweidlem34  42676  smfmullem2  43424  fmtno5lem4  44073  fmtno5  44074  fmtno5faclem2  44097  3ndvds4  44112  139prmALT  44113  31prm  44114  m5prm  44115  11t31e341  44250  2exp340mod341  44251  8exp8mod9  44254  sbgoldbalt  44299  sbgoldbo  44305  nnsum3primesle9  44312  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  ackval3  45097  ackval3012  45106  ackval41a  45108  ackval41  45109  ackval42  45110