Theorem mulid2 9615

Description: Identity law for multiplication. Note: see mulid1 9614 for commuted version. (Contributed by NM, 8-Oct-1999.)

Assertion

Ref	Expression
mulid2

Proof of Theorem mulid2

Step	Hyp	Ref	Expression
1		ax-1cn 9571	. . 3
2		mulcom 9599	. . 3
3	1, 2	mpan 670	. 2
4		mulid1 9614	. 2
5	3, 4	eqtrd 2498	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296  cc 9511  1c1 9514  cmul 9518

This theorem is referenced by:  mulid2i  9620  mulid2d  9635  muladd11  9771  1p1times  9772  mul02lem1  9777  cnegex2  9783  mulm1  10023  div1  10261  recdiv  10275  divdiv2  10281  conjmul  10286  ser1const  12163  expp1  12173  recan  13169  arisum  13671  geo2sum  13682  prodrblem  13736  prodmolem2a  13741  sinhval  13889  coshval  13890  demoivreALT  13936  gcdadd  14168  gcdid  14169  cncrng  18439  cnfld1  18443  cnfldmulg  18450  blcvx  21303  icccvx  21450  coeidp  22660  dgrid  22661  quartlem1  23188  asinsinlem  23222  asinsin  23223  atantan  23254  musumsum  23468  brbtwn2  24208  axsegconlem1  24220  ax5seglem1  24231  ax5seglem2  24232  ax5seglem4  24235  ax5seglem5  24236  axeuclid  24266  axcontlem2  24268  axcontlem4  24270  cnrngo  25405  cncvc  25476  subdivcomb2  29106  risefac1  29155  fallfac1  29156  bpoly3  29820  bpoly4  29821  dvcosax  31723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299