![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulid1d | Unicode version |
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mulid1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mulid1 7582 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-resscn 7534 ax-1cn 7535 ax-icn 7537 ax-addcl 7538 ax-mulcl 7540 ax-mulcom 7543 ax-mulass 7545 ax-distr 7546 ax-1rid 7549 ax-cnre 7553 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 |
This theorem is referenced by: muladd11 7712 ltmul1 8166 mulap0 8220 divrecap 8252 diveqap1 8269 conjmulap 8293 apmul1 8352 qapne 9223 divelunit 9568 modqid 9905 q2submod 9941 addmodlteq 9954 expadd 10128 leexp2r 10140 nnlesq 10189 sqoddm1div8 10237 nn0opthlem1d 10259 faclbnd 10280 faclbnd2 10281 faclbnd6 10283 facavg 10285 bcn0 10294 bcn1 10297 hash2iun1dif1 11038 binom11 11044 trireciplem 11058 geosergap 11064 cvgratnnlemnexp 11082 cvgratnnlemmn 11083 efzval 11137 tanaddaplem 11193 tanaddap 11194 cos01gt0 11217 absef 11223 1dvds 11252 bezoutlema 11430 bezoutlemb 11431 gcdmultiple 11451 sqgcd 11460 lcm1 11505 coprmdvds 11516 qredeu 11521 phiprmpw 11640 |
Copyright terms: Public domain | W3C validator |