Theorem 3p1e4 11423

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

Syntax hints:   = wceq 1652  (class class class)co 6842  1c1 10190   + caddc 10192  3c3 11328  4c4 11329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758  df-4 11337

This theorem is referenced by:  7t6e42  11854  8t5e40  11859  9t5e45  11866  fac4  13272  4bc3eq4  13319  hash4  13396  s4len  13928  bpoly4  15072  2exp16  16071  43prm  16102  83prm  16103  317prm  16106  prmo4  16108  1259lem2  16112  1259lem3  16113  1259lem4  16114  1259lem5  16115  2503lem1  16117  2503lem2  16118  4001lem1  16121  4001lem2  16122  4001lem4  16124  4001prm  16125  sincos6thpi  24559  binom4  24868  quartlem1  24875  log2ublem3  24966  log2ub  24967  bclbnd  25296  tgcgr4  25717  upgr4cycl4dv4e  27463  ex-opab  27748  ex-ind-dvds  27777  fib4  30914  fib5  30915  hgt750lem  31180  hgt750lem2  31181  inductionexd  39127  lhe4.4ex1a  39202  stoweidlem26  40880  stoweidlem34  40888  smfmullem2  41639  fmtno5lem4  42144  fmtno5  42145  fmtno5faclem2  42168  3ndvds4  42186  139prmALT  42187  31prm  42188  m5prm  42189  sbgoldbalt  42345  sbgoldbo  42351  nnsum3primesle9  42358  nnsum4primeseven  42364  nnsum4primesevenALTV  42365