Theorem 3p1e4 12302

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

Syntax hints:   = wceq 1540  (class class class)co 7369  1c1 11045   + caddc 11047  3c3 12218  4c4 12219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-4 12227

This theorem is referenced by:  7t6e42  12738  8t5e40  12743  9t5e45  12750  fz0to4untppr  13567  fz0to5un2tp  13568  fac4  14222  hash4  14348  hash7g  14427  s4len  14841  bpoly4  16001  2exp16  17037  43prm  17068  83prm  17069  317prm  17072  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  4001lem1  17087  4001lem2  17088  4001lem4  17090  4001prm  17091  binom4  26736  quartlem1  26743  log2ublem3  26834  log2ub  26835  bclbnd  27167  addsqnreup  27330  tgcgr4  28434  upgr4cycl4dv4e  30087  ex-opab  30334  ex-ind-dvds  30363  evl1deg3  33520  iconstr  33729  cos9thpiminplylem1  33745  fib4  34368  fib5  34369  hgt750lem  34615  hgt750lem2  34616  3lexlogpow5ineq1  42015  3lexlogpow5ineq5  42021  aks4d1p1p5  42036  aks4d1p1  42037  1p3e4  42220  235t711  42266  3cubeslem3l  42647  3cubeslem3r  42648  inductionexd  44117  lhe4.4ex1a  44291  stoweidlem26  45997  stoweidlem34  46005  smfmullem2  46763  2ltceilhalf  47302  fmtno5lem4  47530  fmtno5  47531  fmtno5faclem2  47554  3ndvds4  47569  139prmALT  47570  31prm  47571  m5prm  47572  11t31e341  47706  2exp340mod341  47707  8exp8mod9  47710  sbgoldbalt  47755  sbgoldbo  47761  nnsum3primesle9  47768  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  gpgprismgr4cycllem10  48067  ackval3  48645  ackval3012  48654  ackval41a  48656  ackval41  48657  ackval42  48658