Theorem 2t1e2 12430

Description: 2 times 1 equals 2. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
2t1e2	⊢ (2 · 1) = 2

Proof of Theorem 2t1e2

Step	Hyp	Ref	Expression
1		2cn 12343	. 2 ⊢ 2 ∈ ℂ
2	1	mulridi 11240	1 ⊢ (2 · 1) = 2

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414  1c1 11128   · cmul 11132  2c2 12322

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulcom 11191  ax-mulass 11193  ax-distr 11194  ax-1rid 11197  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12330

This theorem is used by:  decbin2  12887  expubnd  14245  01sqrexlem7  15338  trirecip  15955  bpoly3  16147  fsumcube  16149  ege2le3  16179  cos2tsin  16270  cos2bnd  16279  odd2np1  16434  opoe  16456  flodddiv4  16508  2mulprm  16786  pythagtriplem4  16914  2503lem2  17233  2503lem3  17234  4001lem4  17239  4001prm  17240  htpycc  25211  pco1  25246  pcohtpylem  25250  pcopt  25253  pcorevlem  25257  ovolunlem1a  25727  cos2pi  26717  coskpi  26763  dcubic2  27084  dcubic  27086  basellem3  27322  chtublem  27450  bcp1ctr  27518  bclbnd  27519  bposlem1  27523  bposlem2  27524  bposlem5  27527  2lgslem3d1  27642  2sqreultlem  27686  2sqreunnltlem  27689  chebbnd1lem1  27708  chebbnd1lem3  27710  chebbnd1  27711  frgrregord013  30878  ex-ind-dvds  30944  wrdt2ind  33398  knoppndvlem12  37223  heiborlem6  38569  3lexlogpow5ineq1  42923  aks4d1p1  42945  2np3bcnp1  43013  2ap1caineq  43014  flt4lem7  43508  jm2.23  43840  sumnnodd  46463  wallispilem4  46899  wallispi2lem1  46902  wallispi2lem2  46903  wallispi2  46904  stirlinglem11  46915  dirkertrigeqlem1  46929  fouriersw  47062  goldratval  47757  fmtnorec4  48455  lighneallem2  48512  lighneallem3  48513  3exp4mod41  48522  opoeALTV  48602  fppr2odd  48650  8exp8mod9  48655  ackval2  49615  ackval2012  49624