Theorem 3p1e4 11365

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

Syntax hints:   = wceq 1632  (class class class)co 6814  1c1 10149   + caddc 10151  3c3 11283  4c4 11284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-4 11293

This theorem is referenced by:  7t6e42  11864  8t5e40  11869  8t5e40OLD  11870  9t5e45  11878  fac4  13282  4bc3eq4  13329  hash4  13407  s4len  13864  bpoly4  15009  2exp16  16019  43prm  16051  83prm  16052  317prm  16055  prmo4  16057  1259lem2  16061  1259lem3  16062  1259lem4  16063  1259lem5  16064  2503lem1  16066  2503lem2  16067  4001lem1  16070  4001lem2  16071  4001lem4  16073  4001prm  16074  sincos6thpi  24487  binom4  24797  quartlem1  24804  log2ublem3  24895  log2ub  24896  bclbnd  25225  tgcgr4  25646  upgr4cycl4dv4e  27358  ex-opab  27621  ex-ind-dvds  27650  fib4  30796  fib5  30797  hgt750lem  31059  hgt750lem2  31060  inductionexd  38973  lhe4.4ex1a  39048  stoweidlem26  40764  stoweidlem34  40772  smfmullem2  41523  fmtno5lem4  41996  fmtno5  41997  fmtno5faclem2  42020  3ndvds4  42038  139prmALT  42039  31prm  42040  m5prm  42041  sbgoldbalt  42197  sbgoldbo  42203  nnsum3primesle9  42210  nnsum4primeseven  42216  nnsum4primesevenALTV  42217