Theorem 3t2e6 12433

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 12349	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12406	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12419	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2783	1 ⊢ (3 · 2) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7414   + caddc 11130   · cmul 11132  2c2 12322  3c3 12323  6c6 12326

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-addass 11192  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  df-3 12331  df-4 12332  df-5 12333  df-6 12334

This theorem is used by:  2t3e6  12434  3t3e9  12435  bpoly3  16147  bpoly4  16148  sin01bnd  16276  3lcm2e6woprm  16708  3lcm2e6  16826  6nprm  17204  7prm  17205  17prm  17212  37prm  17216  83prm  17218  163prm  17220  317prm  17221  631prm  17222  1259lem4  17229  2503lem2  17233  4001lem1  17236  4001lem3  17238  4001prm  17240  sincos6thpi  26756  pigt3  26758  log2ublem3  27188  log2ub  27189  basellem5  27324  ppiublem1  27441  bclbnd  27519  bpos1  27522  bposlem9  27531  2lgslem3d  27638  cos9thpiminplylem4  34298  cos9thpiminplylem5  34299  hgt750lem2  35163  problem4  36250  problem5  36251  3cubeslem3l  43534  3cubeslem3r  43535  lhe4.4ex1a  45156  stoweidlem13  46844  sin5tlem1  47740  sin5tlem4  47743  ceil5half3  48237  minusmodnep2tmod  48250  257prm  48467  127prm  48505  ppivalnn4  48533  6even  48630  2exp340mod341  48652  2t6m3t4e0  49281  zlmodzxzequa  49429