Theorem 3p1e4 12312

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

Syntax hints:   = wceq 1547  (class class class)co 7356  1c1 11030   + caddc 11032  3c3 12228  4c4 12229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-4 12237

This theorem is referenced by:  7t6e42  12748  8t5e40  12753  9t5e45  12760  fz0to4untppr  13575  fz0to5un2tp  13576  fac4  14234  hash4  14360  hash7g  14439  s4len  14852  bpoly4  16015  2exp16  17052  43prm  17083  83prm  17084  317prm  17087  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  2503lem1  17098  2503lem2  17099  4001lem1  17102  4001lem2  17103  4001lem4  17105  4001prm  17106  binom4  26832  quartlem1  26839  log2ublem3  26930  log2ub  26931  bclbnd  27261  addsqnreup  27424  tgcgr4  28617  upgr4cycl4dv4e  30273  ex-opab  30520  ex-ind-dvds  30549  evl1deg3  33661  iconstr  33950  cos9thpiminplylem1  33966  fib4  34588  fib5  34589  hgt750lem  34835  hgt750lem2  34836  3lexlogpow5ineq1  42539  3lexlogpow5ineq5  42545  aks4d1p1p5  42560  aks4d1p1  42561  1p3e4  42742  235t711  42782  3cubeslem3l  43135  3cubeslem3r  43136  inductionexd  44599  lhe4.4ex1a  44773  stoweidlem26  46469  stoweidlem34  46477  smfmullem2  47235  2ltceilhalf  47795  fmtno5lem4  48034  fmtno5  48035  fmtno5faclem2  48058  3ndvds4  48073  139prmALT  48074  31prm  48075  m5prm  48076  ppivalnnnprm  48106  11t31e341  48223  2exp340mod341  48224  8exp8mod9  48227  sbgoldbalt  48272  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  gpgprismgr4cycllem10  48595  ackval3  49174  ackval3012  49183  ackval41a  49185  ackval41  49186  ackval42  49187