Theorem 3p1e4 11153

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

Syntax hints:   = wceq 1483  (class class class)co 6650  1c1 9937   + caddc 9939  3c3 11071  4c4 11072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-4 11081

This theorem is referenced by:  7t6e42  11652  8t5e40  11657  8t5e40OLD  11658  9t5e45  11666  fac4  13068  4bc3eq4  13115  hash4  13195  s4len  13644  bpoly4  14790  2exp16  15797  43prm  15829  83prm  15830  317prm  15833  prmo4  15835  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  2503lem1  15844  2503lem2  15845  4001lem1  15848  4001lem2  15849  4001lem4  15851  4001prm  15852  sincos6thpi  24267  binom4  24577  quartlem1  24584  log2ublem3  24675  log2ub  24676  bclbnd  25005  tgcgr4  25426  upgr4cycl4dv4e  27045  ex-opab  27289  ex-ind-dvds  27318  fib4  30466  fib5  30467  hgt750lem  30729  hgt750lem2  30730  inductionexd  38453  lhe4.4ex1a  38528  stoweidlem26  40243  stoweidlem34  40251  smfmullem2  40999  fmtno5lem4  41468  fmtno5  41469  fmtno5faclem2  41492  3ndvds4  41510  139prmALT  41511  31prm  41512  m5prm  41513  sbgoldbalt  41669  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primeseven  41688  nnsum4primesevenALTV  41689