![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulridi | GIF version |
Description: Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
mulridi | ⊢ (𝐴 · 1) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | mulrid 8021 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 · 1) = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 ∈ wcel 2167 (class class class)co 5922 ℂcc 7875 1c1 7878 · cmul 7882 |
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 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-ext 2178 ax-resscn 7969 ax-1cn 7970 ax-icn 7972 ax-addcl 7973 ax-mulcl 7975 ax-mulcom 7978 ax-mulass 7980 ax-distr 7981 ax-1rid 7984 ax-cnre 7988 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 df-rex 2481 df-v 2765 df-un 3161 df-in 3163 df-ss 3170 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-br 4034 df-iota 5219 df-fv 5266 df-ov 5925 |
This theorem is referenced by: rimul 8609 muleqadd 8692 1t1e1 9140 2t1e2 9141 3t1e3 9143 halfpm6th 9208 iap0 9211 9p1e10 9456 numltc 9479 numsucc 9493 dec10p 9496 numadd 9500 numaddc 9501 11multnc 9521 4t3lem 9550 5t2e10 9553 9t11e99 9583 rei 11049 imi 11050 cji 11052 0.999... 11670 efival 11881 ef01bndlem 11905 3lcm2e6 12304 decsplit0b 12571 2exp8 12580 dveflem 14938 efhalfpi 15008 |
Copyright terms: Public domain | W3C validator |