Theorem 3p1e4 12438

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

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  3c3 12349  4c4 12350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-4 12358

This theorem is referenced by:  7t6e42  12871  8t5e40  12876  9t5e45  12883  fz0to4untppr  13687  fz0to5un2tp  13688  fac4  14330  hash4  14456  hash7g  14535  s4len  14948  bpoly4  16107  2exp16  17138  43prm  17169  83prm  17170  317prm  17173  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  4001lem1  17188  4001lem2  17189  4001lem4  17191  4001prm  17192  binom4  26911  quartlem1  26918  log2ublem3  27009  log2ub  27010  bclbnd  27342  addsqnreup  27505  tgcgr4  28557  upgr4cycl4dv4e  30217  ex-opab  30464  ex-ind-dvds  30493  evl1deg3  33568  fib4  34369  fib5  34370  hgt750lem  34628  hgt750lem2  34629  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1p5  42032  aks4d1p1  42033  235t711  42293  3cubeslem3l  42642  3cubeslem3r  42643  inductionexd  44117  lhe4.4ex1a  44298  stoweidlem26  45947  stoweidlem34  45955  smfmullem2  46713  fmtno5lem4  47430  fmtno5  47431  fmtno5faclem2  47454  3ndvds4  47469  139prmALT  47470  31prm  47471  m5prm  47472  11t31e341  47606  2exp340mod341  47607  8exp8mod9  47610  sbgoldbalt  47655  sbgoldbo  47661  nnsum3primesle9  47668  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  ackval3  48417  ackval3012  48426  ackval41a  48428  ackval41  48429  ackval42  48430