Theorem 3t2e6 12508

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 12424	. . 3 ⊢ 3 ∈ ℂ
2	1	times2i 12481	. 2 ⊢ (3 · 2) = (3 + 3)
3		3p3e6 12494	. 2 ⊢ (3 + 3) = 6
4	2, 3	eqtri 2784	1 ⊢ (3 · 2) = 6

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7420   + caddc 11203   · cmul 11205  2c2 12397  3c3 12398  6c6 12401

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 2733  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-1rid 11270  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409

This theorem is used by:  2t3e6  12509  3t3e9  12510  bpoly3  16224  bpoly4  16225  sin01bnd  16353  3lcm2e6woprm  16790  3lcm2e6  16908  6nprm  17287  7prm  17288  17prm  17295  37prm  17299  83prm  17301  163prm  17303  317prm  17304  631prm  17305  1259lem4  17312  2503lem2  17316  4001lem1  17319  4001lem3  17321  4001prm  17323  sincos6thpi  26844  pigt3  26846  log2ublem3  27276  log2ub  27277  basellem5  27412  ppiublem1  27529  bclbnd  27607  bpos1  27610  bposlem9  27619  2lgslem3d  27726  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  hgt750lem2  35281  problem4  36433  problem5  36434  3cubeslem3l  43696  3cubeslem3r  43697  lhe4.4ex1a  45312  stoweidlem13  47022  sin5tlem1  47918  sin5tlem4  47921  ceil5half3  48415  minusmodnep2tmod  48428  257prm  48645  127prm  48683  ppivalnn4  48711  6even  48808  2exp340mod341  48830  2t6m3t4e0  49459  zlmodzxzequa  49607