Theorem 3p1e4 12380

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

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   + caddc 11098  3c3 12291  4c4 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-4 12300

This theorem is referenced by:  7t6e42  12824  8t5e40  12829  9t5e45  12836  fz0to4untppr  13654  fz0to5un2tp  13655  fac4  14313  hash4  14439  hash7g  14519  s4len  14932  bpoly4  16108  2exp16  17145  43prm  17177  83prm  17178  317prm  17181  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  4001lem1  17196  4001lem2  17197  4001lem4  17199  4001prm  17200  binom4  27015  quartlem1  27022  log2ublem3  27113  log2ub  27114  bclbnd  27444  addsqnreup  27607  tgcgr4  28800  upgr4cycl4dv4e  30536  ex-opab  30783  ex-ind-dvds  30812  evl1deg3  33868  iconstr  34156  cos9thpiminplylem1  34172  fib4  34794  fib5  34795  hgt750lem  35038  hgt750lem2  35039  3lexlogpow5ineq1  42821  3lexlogpow5ineq5  42827  aks4d1p1p5  42842  aks4d1p1  42843  1p3e4  43026  235t711  43066  3cubeslem3l  43417  3cubeslem3r  43418  inductionexd  44881  lhe4.4ex1a  45039  stoweidlem26  46740  stoweidlem34  46748  smfmullem2  47506  2ltceilhalf  48069  fmtno5lem4  48308  fmtno5  48309  fmtno5faclem2  48332  3ndvds4  48347  139prmALT  48348  31prm  48349  m5prm  48350  ppivalnnnprm  48380  11t31e341  48497  2exp340mod341  48498  8exp8mod9  48501  sbgoldbalt  48546  sbgoldbo  48552  nnsum3primesle9  48559  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  gpgprismgr4cycllem10  48869  ackval3  49463  ackval3012  49472  ackval41a  49474  ackval41  49475  ackval42  49476