MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2times Unicode version

Theorem 2times 10679
Description: Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.)
Assertion
Ref Expression
2times

Proof of Theorem 2times
StepHypRef Expression
1 df-2 10619 . . 3
21oveq1i 6306 . 2
3 1p1times 9772 . 2
42, 3syl5eq 2510 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511  1c1 9514   caddc 9516   cmul 9518  2c2 10610
This theorem is referenced by:  times2  10680  2timesi  10681  2halves  10792  halfaddsub  10797  avglt2  10802  2timesd  10806  expubnd  12226  subsq2  12276  absmax  13162  sinmul  13907  sin2t  13912  cos2t  13913  sadadd2lem2  14100  pythagtriplem4  14343  pythagtriplem14  14352  pythagtriplem16  14354  cncph  25734  pellexlem2  30766  acongrep  30918  sub2times  31455  2timesgt  31475  2txmxeqx  32317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619
  Copyright terms: Public domain W3C validator