ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulid1d Unicode version

Theorem mulid1d 7751
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mulid1d  |-  ( ph  ->  ( A  x.  1 )  =  A )

Proof of Theorem mulid1d
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mulid1 7731 . 2  |-  ( A  e.  CC  ->  ( A  x.  1 )  =  A )
31, 2syl 14 1  |-  ( ph  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465  (class class class)co 5742   CCcc 7586   1c1 7589    x. cmul 7593
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-resscn 7680  ax-1cn 7681  ax-icn 7683  ax-addcl 7684  ax-mulcl 7686  ax-mulcom 7689  ax-mulass 7691  ax-distr 7692  ax-1rid 7695  ax-cnre 7699
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  muladd11  7863  ltmul1  8322  mulap0  8383  divrecap  8416  diveqap1  8433  conjmulap  8457  apmul1  8516  qapne  9399  divelunit  9753  modqid  10090  q2submod  10126  addmodlteq  10139  expadd  10303  leexp2r  10315  nnlesq  10364  sqoddm1div8  10412  nn0opthlem1d  10434  faclbnd  10455  faclbnd2  10456  faclbnd6  10458  facavg  10460  bcn0  10469  bcn1  10472  reccn2ap  11050  hash2iun1dif1  11217  binom11  11223  trireciplem  11237  geosergap  11243  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  efzval  11316  tanaddaplem  11372  tanaddap  11373  cos01gt0  11396  absef  11403  1dvds  11434  bezoutlema  11614  bezoutlemb  11615  gcdmultiple  11635  sqgcd  11644  lcm1  11689  coprmdvds  11700  qredeu  11705  phiprmpw  11825  dveflem  12782  efper  12815  tangtx  12846  trilpolemclim  13156  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator