Theorem mulid2i 7927

Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)

Hypothesis

Ref	Expression
axi.1	|- A e. CC

Assertion

Ref	Expression
mulid2i	|- ( 1 x. A ) = A

Proof of Theorem mulid2i

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		mulid2 7922	. 2 |- ( A e. CC -> ( 1 x. A ) = A )
3	1, 2	ax-mp 5	1 |- ( 1 x. A ) = A

Syntax hints:   = wceq 1349   e. wcel 2142  (class class class)co 5857   CCcc 7776   1c1 7779   x. cmul 7783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153  ax-resscn 7870  ax-1cn 7871  ax-icn 7873  ax-addcl 7874  ax-mulcl 7876  ax-mulcom 7879  ax-mulass 7881  ax-distr 7882  ax-1rid 7885  ax-cnre 7889

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-iota 5162  df-fv 5208  df-ov 5860

This theorem is referenced by:  halfpm6th  9102  div4p1lem1div2  9135  3halfnz  9313  sq10  10650  fac2  10669  efival  11699  ef01bndlem  11723  3dvdsdec  11828  3dvds2dec  11829  odd2np1lem  11835  m1expo  11863  m1exp1  11864  nno  11869  sin2pim  13613  cos2pim  13614  sincosq3sgn  13628  sincosq4sgn  13629  cosq23lt0  13633  tangtx  13638  sincosq1eq  13639  sincos4thpi  13640  sincos6thpi  13642  abssinper  13646  cosq34lt1  13650  lgsdir2lem1  13808  lgsdir2lem4  13811  lgsdir2lem5  13812  ex-fl  13845