Theorem 6p1e7 12383

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 12303	. 2 ⊢ 7 = (6 + 1)
2	1	eqcomi 2772	1 ⊢ (6 + 1) = 7

Syntax hints:   = wceq 1570  (class class class)co 7410  1c1 11096   + caddc 11098  6c6 12294  7c7 12295

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

This theorem is referenced by:  9t8e72  12839  s7len  14935  37prm  17176  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem3  17188  1259lem4  17189  1259lem5  17190  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem4  17199  4001prm  17200  log2ublem3  27113  log2ub  27114  hgt750lemd  35035  hgt750lem2  35039  3exp7  42820  3lexlogpow5ineq1  42821  25or6to4  42973  235t711  43066  ex-decpmul  43067  3cubeslem3l  43417  3cubeslem3r  43418  fmtno2  48302  fmtno3  48303  fmtno4  48304  fmtno5lem4  48308  fmtno5  48309  fmtno4nprmfac193  48326  fmtno5fac  48334  127prm  48351  mod42tp1mod8  48354  ppivalnn4  48379  2exp340mod341  48498  gbowge7  48528  sbgoldbwt  48542  nnsum3primesle9  48559