Theorem mulridd 7971

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 7951	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 · 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5872  ℂcc 7806  1c1 7809   · cmul 7813

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 7900  ax-1cn 7901  ax-icn 7903  ax-addcl 7904  ax-mulcl 7906  ax-mulcom 7909  ax-mulass 7911  ax-distr 7912  ax-1rid 7915  ax-cnre 7919

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 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4003  df-iota 5177  df-fv 5223  df-ov 5875

This theorem is referenced by:  muladd11  8086  ltmul1  8545  mulap0  8607  divrecap  8641  diveqap1  8658  conjmulap  8682  apmul1  8741  qapne  9635  divelunit  9998  modqid  10344  q2submod  10380  addmodlteq  10393  expadd  10557  leexp2r  10569  nnlesq  10618  sqoddm1div8  10668  nn0opthlem1d  10693  faclbnd  10714  faclbnd2  10715  faclbnd6  10717  facavg  10719  bcn0  10728  bcn1  10731  reccn2ap  11314  hash2iun1dif1  11481  binom11  11487  trireciplem  11501  geosergap  11507  cvgratnnlemnexp  11525  cvgratnnlemmn  11526  fprodsplitdc  11597  efzval  11684  tanaddaplem  11739  tanaddap  11740  cos01gt0  11763  absef  11770  1dvds  11805  bezoutlema  11992  bezoutlemb  11993  gcdmultiple  12013  sqgcd  12022  lcm1  12073  coprmdvds  12084  qredeu  12089  phiprmpw  12214  coprimeprodsq  12249  pc2dvds  12321  sumhashdc  12337  fldivp1  12338  pcfaclem  12339  prmpwdvds  12345  zsssubrg  13348  dveflem  14058  efper  14099  tangtx  14130  logdivlti  14173  relogbexpap  14247  rplogbcxp  14252  lgsdir2  14305  2sqlem6  14327  2sqlem8  14330  trilpolemclim  14644  trilpolemisumle  14646  trilpolemeq1  14648  trilpolemlt1  14649  redcwlpolemeq1  14662  nconstwlpolemgt0  14671