Theorem 6p1e7 12441

Description: 6 + 1 = 7. (Contributed by Mario Carneiro, 18-Apr-2015.)

Assertion

Ref	Expression
6p1e7	⊢ (6 + 1) = 7

Proof of Theorem 6p1e7

Step	Hyp	Ref	Expression
1		df-7 12361	. 2 ⊢ 7 = (6 + 1)
2	1	eqcomi 2749	1 ⊢ (6 + 1) = 7

Syntax hints:   = wceq 1537  (class class class)co 7448  1c1 11185   + caddc 11187  6c6 12352  7c7 12353

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-7 12361

This theorem is referenced by:  9t8e72  12886  s7len  14951  37prm  17168  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem4  17191  4001prm  17192  log2ublem3  27009  log2ub  27010  hgt750lemd  34625  hgt750lem2  34629  3exp7  42010  3lexlogpow5ineq1  42011  235t711  42293  ex-decpmul  42294  3cubeslem3l  42642  3cubeslem3r  42643  fmtno2  47424  fmtno3  47425  fmtno4  47426  fmtno5lem4  47430  fmtno5  47431  fmtno4nprmfac193  47448  fmtno5fac  47456  127prm  47473  mod42tp1mod8  47476  2exp340mod341  47607  gbowge7  47637  sbgoldbwt  47651  nnsum3primesle9  47668