Theorem 3p1e4 12384

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

Syntax hints:   = wceq 1567  (class class class)co 7411  1c1 11100   + caddc 11102  3c3 12295  4c4 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-4 12304

This theorem is referenced by:  7t6e42  12828  8t5e40  12833  9t5e45  12840  fz0to4untppr  13657  fz0to5un2tp  13658  fac4  14316  hash4  14442  hash7g  14522  s4len  14935  bpoly4  16112  2exp16  17149  43prm  17181  83prm  17182  317prm  17185  1259lem2  17191  1259lem3  17192  1259lem4  17193  1259lem5  17194  2503lem1  17196  2503lem2  17197  4001lem1  17200  4001lem2  17201  4001lem4  17203  4001prm  17204  binom4  26980  quartlem1  26987  log2ublem3  27078  log2ub  27079  bclbnd  27409  addsqnreup  27572  tgcgr4  28765  upgr4cycl4dv4e  30476  ex-opab  30723  ex-ind-dvds  30752  evl1deg3  33812  iconstr  34100  cos9thpiminplylem1  34116  fib4  34738  fib5  34739  hgt750lem  34982  hgt750lem2  34983  3lexlogpow5ineq1  42710  3lexlogpow5ineq5  42716  aks4d1p1p5  42731  aks4d1p1  42732  1p3e4  42915  235t711  42955  3cubeslem3l  43308  3cubeslem3r  43309  inductionexd  44772  lhe4.4ex1a  44930  stoweidlem26  46631  stoweidlem34  46639  smfmullem2  47397  2ltceilhalf  47957  fmtno5lem4  48196  fmtno5  48197  fmtno5faclem2  48220  3ndvds4  48235  139prmALT  48236  31prm  48237  m5prm  48238  ppivalnnnprm  48268  11t31e341  48385  2exp340mod341  48386  8exp8mod9  48389  sbgoldbalt  48434  sbgoldbo  48440  nnsum3primesle9  48447  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  gpgprismgr4cycllem10  48757  ackval3  49347  ackval3012  49356  ackval41a  49358  ackval41  49359  ackval42  49360