Theorem 3t2e6 12423

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 12339	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12396	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12409	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2788	1 ⊢ (3 · 2) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7419   + caddc 11120   · cmul 11122  2c2 12312  3c3 12313  6c6 12316

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 2148  ax-9 2156  ax-ext 2737  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-1rid 11187  ax-cnre 11190

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 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324

This theorem is used by:  2t3e6  12424  3t3e9  12425  bpoly3  16136  bpoly4  16137  sin01bnd  16265  3lcm2e6woprm  16697  3lcm2e6  16815  6nprm  17193  7prm  17194  17prm  17201  37prm  17205  83prm  17207  163prm  17209  317prm  17210  631prm  17211  1259lem4  17218  2503lem2  17222  4001lem1  17225  4001lem3  17227  4001prm  17229  sincos6thpi  26734  pigt3  26736  log2ublem3  27166  log2ub  27167  basellem5  27302  ppiublem1  27419  bclbnd  27497  bpos1  27500  bposlem9  27509  2lgslem3d  27616  cos9thpiminplylem4  34241  cos9thpiminplylem5  34242  hgt750lem2  35106  problem4  36199  problem5  36200  3cubeslem3l  43477  3cubeslem3r  43478  lhe4.4ex1a  45099  stoweidlem13  46787  sin5tlem1  47670  sin5tlem4  47673  ceil5half3  48143  minusmodnep2tmod  48156  257prm  48373  127prm  48411  ppivalnn4  48439  6even  48536  2exp340mod341  48558  2t6m3t4e0  49187  zlmodzxzequa  49335