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  26793  quartlem1  26800  log2ublem3  26891  log2ub  26892  bclbnd  27224  addsqnreup  27387  tgcgr4  28511  upgr4cycl4dv4e  30164  ex-opab  30411  ex-ind-dvds  30440  evl1deg3  33540  iconstr  33749  cos9thpiminplylem1  33765  fib4  34388  fib5  34389  hgt750lem  34635  hgt750lem2  34636  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1p5  42056  aks4d1p1  42057  1p3e4  42240  235t711  42286  3cubeslem3l  42667  3cubeslem3r  42668  inductionexd  44137  lhe4.4ex1a  44311  stoweidlem26  46017  stoweidlem34  46025  smfmullem2  46783  2ltceilhalf  47322  fmtno5lem4  47550  fmtno5  47551  fmtno5faclem2  47574  3ndvds4  47589  139prmALT  47590  31prm  47591  m5prm  47592  11t31e341  47726  2exp340mod341  47727  8exp8mod9  47730  sbgoldbalt  47775  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  gpgprismgr4cycllem10  48087  ackval3  48665  ackval3012  48674  ackval41a  48676  ackval41  48677  ackval42  48678