Theorem 3t2e6 12518

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 12434	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12491	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12504	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2786	1 ⊢ (3 · 2) = 6

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7427   + caddc 11213   · cmul 11215  2c2 12407  3c3 12408  6c6 12411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-mulcl 11272  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-1rid 11280  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419

This theorem is used by:  2t3e6  12519  3t3e9  12520  bpoly3  16236  bpoly4  16237  sin01bnd  16365  3lcm2e6woprm  16802  3lcm2e6  16920  6nprm  17299  7prm  17300  17prm  17307  37prm  17311  83prm  17313  163prm  17315  317prm  17316  631prm  17317  1259lem4  17324  2503lem2  17328  4001lem1  17331  4001lem3  17333  4001prm  17335  sincos6thpi  26856  pigt3  26858  log2ublem3  27288  log2ub  27289  basellem5  27424  ppiublem1  27541  bclbnd  27619  bpos1  27622  bposlem9  27631  2lgslem3d  27738  cos9thpiminplylem4  34470  cos9thpiminplylem5  34471  hgt750lem2  35334  problem4  36554  problem5  36555  3cubeslem3l  43836  3cubeslem3r  43837  lhe4.4ex1a  45453  stoweidlem13  47162  sin5tlem1  48058  sin5tlem4  48061  ceil5half3  48555  minusmodnep2tmod  48568  257prm  48785  127prm  48823  ppivalnn4  48851  6even  48948  2exp340mod341  48970  2t6m3t4e0  49599  zlmodzxzequa  49747