Theorem 3t2e6 12286

Description: 3 times 2 equals 6. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
3t2e6	⊢ (3 · 2) = 6

Proof of Theorem 3t2e6

Step	Hyp	Ref	Expression
1		3cn 12206	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12259	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12272	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2754	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1541  (class class class)co 7346   + caddc 11009   · cmul 11011  2c2 12180  3c3 12181  6c6 12184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-1rid 11076  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192

This theorem is referenced by:  3t3e9  12287  8th4div3  12341  halfthird  12342  fac3  14187  bpoly3  15965  bpoly4  15966  sin01bnd  16094  3lcm2e6woprm  16526  3lcm2e6  16643  prmo3  16953  2exp6  16998  6nprm  17021  7prm  17022  17prm  17028  37prm  17032  83prm  17034  163prm  17036  317prm  17037  631prm  17038  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem2  17049  4001lem1  17052  4001lem3  17054  4001prm  17056  sincos6thpi  26452  pigt3  26454  quart1  26793  log2ublem2  26884  log2ublem3  26885  log2ub  26886  basellem5  27022  basellem8  27025  cht3  27110  ppiublem1  27140  ppiub  27142  bclbnd  27218  bpos1  27221  bposlem8  27229  bposlem9  27230  2lgslem3d  27337  2lgsoddprmlem3d  27351  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  hgt750lem2  34665  problem4  35712  problem5  35713  3exp7  42156  3cubeslem3l  42789  3cubeslem3r  42790  lhe4.4ex1a  44432  stoweidlem13  46121  ceil5half3  47450  minusmodnep2tmod  47463  257prm  47671  127prm  47709  mod42tp1mod8  47712  6even  47821  2exp340mod341  47843  2t6m3t4e0  48458  zlmodzxzequa  48607