Theorem 3t2e6 12406

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 12322	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12379	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12392	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2792	1 ⊢ (3 · 2) = 6

Syntax hints:   = wceq 1567  (class class class)co 7411   + caddc 11103   · cmul 11105  2c2 12295  3c3 12296  6c6 12299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-1rid 11170  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307

This theorem is referenced by:  2t3e6  12407  3t3e9  12408  8th4div3  12464  halfthird  12465  fac3  14316  bpoly3  16112  bpoly4  16113  sin01bnd  16241  3lcm2e6woprm  16673  3lcm2e6  16791  prmo3  17101  2exp6  17146  6nprm  17169  7prm  17170  17prm  17177  37prm  17181  83prm  17183  163prm  17185  317prm  17186  631prm  17187  1259lem3  17193  1259lem4  17194  1259lem5  17195  2503lem2  17198  4001lem1  17201  4001lem3  17203  4001prm  17205  sincos6thpi  26647  pigt3  26649  quart1  26987  log2ublem2  27078  log2ublem3  27079  log2ub  27080  basellem5  27215  basellem8  27218  ppiublem1  27332  ppiub  27334  bclbnd  27410  bpos1  27413  bposlem8  27421  bposlem9  27422  2lgslem3d  27529  2lgsoddprmlem3d  27543  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  hgt750lem2  34984  problem4  36059  problem5  36060  3exp7  42710  3cubeslem3l  43309  3cubeslem3r  43310  lhe4.4ex1a  44931  stoweidlem13  46619  sin5tlem1  47499  sin5tlem4  47502  ceil5half3  47972  minusmodnep2tmod  47985  257prm  48202  127prm  48240  ppivalnn4  48268  6even  48365  2exp340mod341  48387  2t6m3t4e0  49013  zlmodzxzequa  49161