Theorem 3p1e4 12326

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

Syntax hints:   = wceq 1540  (class class class)co 7387  1c1 11069   + caddc 11071  3c3 12242  4c4 12243

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 12251

This theorem is referenced by:  7t6e42  12762  8t5e40  12767  9t5e45  12774  fz0to4untppr  13591  fz0to5un2tp  13592  fac4  14246  hash4  14372  hash7g  14451  s4len  14865  bpoly4  16025  2exp16  17061  43prm  17092  83prm  17093  317prm  17096  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  4001lem1  17111  4001lem2  17112  4001lem4  17114  4001prm  17115  binom4  26760  quartlem1  26767  log2ublem3  26858  log2ub  26859  bclbnd  27191  addsqnreup  27354  tgcgr4  28458  upgr4cycl4dv4e  30114  ex-opab  30361  ex-ind-dvds  30390  evl1deg3  33547  iconstr  33756  cos9thpiminplylem1  33772  fib4  34395  fib5  34396  hgt750lem  34642  hgt750lem2  34643  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p5  42063  aks4d1p1  42064  1p3e4  42247  235t711  42293  3cubeslem3l  42674  3cubeslem3r  42675  inductionexd  44144  lhe4.4ex1a  44318  stoweidlem26  46024  stoweidlem34  46032  smfmullem2  46790  2ltceilhalf  47329  fmtno5lem4  47557  fmtno5  47558  fmtno5faclem2  47581  3ndvds4  47596  139prmALT  47597  31prm  47598  m5prm  47599  11t31e341  47733  2exp340mod341  47734  8exp8mod9  47737  sbgoldbalt  47782  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  gpgprismgr4cycllem10  48094  ackval3  48672  ackval3012  48681  ackval41a  48683  ackval41  48684  ackval42  48685