![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulid2d | Unicode version |
Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mulid2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mulid2 7476 |
. 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 104 ax-ia2 105 ax-ia3 106 ax-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-resscn 7427 ax-1cn 7428 ax-icn 7430 ax-addcl 7431 ax-mulcl 7433 ax-mulcom 7436 ax-mulass 7438 ax-distr 7439 ax-1rid 7442 ax-cnre 7446 |
This theorem depends on definitions: df-bi 115 df-3an 926 df-tru 1292 df-nf 1395 df-sb 1693 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ral 2364 df-rex 2365 df-v 2621 df-un 3003 df-in 3005 df-ss 3012 df-sn 3450 df-pr 3451 df-op 3453 df-uni 3652 df-br 3844 df-iota 4975 df-fv 5018 df-ov 5647 |
This theorem is referenced by: adddirp1d 7504 mulsubfacd 7886 mulcanapd 8120 receuap 8128 divdivdivap 8170 divcanap5 8171 ltrec 8334 recp1lt1 8350 nndivtr 8454 xp1d2m1eqxm1d2 8658 gtndiv 8831 lincmb01cmp 9410 iccf1o 9411 modqfrac 9732 qnegmod 9764 addmodid 9767 m1expcl2 9965 expgt1 9981 ltexp2a 9995 leexp2a 9996 binom3 10059 faclbnd 10137 facavg 10142 ibcval5 10159 cvg1nlemcau 10405 resqrexlemover 10431 resqrexlemcalc2 10436 absimle 10505 maxabslemlub 10628 binom1p 10866 binom1dif 10868 efcllemp 10935 ef01bndlem 11034 efieq1re 11048 eirraplem 11051 iddvds 11074 gcdaddm 11240 rpmulgcd 11280 prmind2 11367 phiprm 11464 hashgcdlem 11468 qdencn 11798 |
Copyright terms: Public domain | W3C validator |