Theorem mulridd 7976

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
mulridd	⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Proof of Theorem mulridd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mulrid 7956	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811  1c1 7814   · cmul 7818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7905  ax-1cn 7906  ax-icn 7908  ax-addcl 7909  ax-mulcl 7911  ax-mulcom 7914  ax-mulass 7916  ax-distr 7917  ax-1rid 7920  ax-cnre 7924

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  muladd11  8092  ltmul1  8551  mulap0  8613  divrecap  8647  diveqap1  8664  conjmulap  8688  apmul1  8747  qapne  9641  divelunit  10004  modqid  10351  q2submod  10387  addmodlteq  10400  expadd  10564  leexp2r  10576  nnlesq  10626  sqoddm1div8  10676  nn0opthlem1d  10702  faclbnd  10723  faclbnd2  10724  faclbnd6  10726  facavg  10728  bcn0  10737  bcn1  10740  reccn2ap  11323  hash2iun1dif1  11490  binom11  11496  trireciplem  11510  geosergap  11516  cvgratnnlemnexp  11534  cvgratnnlemmn  11535  fprodsplitdc  11606  efzval  11693  tanaddaplem  11748  tanaddap  11749  cos01gt0  11772  absef  11779  1dvds  11814  bezoutlema  12002  bezoutlemb  12003  gcdmultiple  12023  sqgcd  12032  lcm1  12083  coprmdvds  12094  qredeu  12099  phiprmpw  12224  coprimeprodsq  12259  pc2dvds  12331  sumhashdc  12347  fldivp1  12348  pcfaclem  12349  prmpwdvds  12355  zsssubrg  13564  dveflem  14272  efper  14313  tangtx  14344  logdivlti  14387  relogbexpap  14461  rplogbcxp  14466  lgsdir2  14519  2sqlem6  14552  2sqlem8  14555  trilpolemclim  14869  trilpolemisumle  14871  trilpolemeq1  14873  trilpolemlt1  14874  redcwlpolemeq1  14887  nconstwlpolemgt0  14897