![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anidms | Unicode version |
Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
Ref | Expression |
---|---|
anidms.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anidms |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidms.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm2.43i 49 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: sylancb 418 sylancbr 419 intsng 3893 pwnss 4177 posng 4716 sqxpexg 4760 xpid11 4868 resiexg 4970 f1mpt 5793 f1eqcocnv 5813 isopolem 5844 poxp 6257 nnmsucr 6513 erex 6583 ecopover 6659 ecopoverg 6662 enrefg 6790 3xpfi 6959 tapeq2 7282 netap 7283 2omotaplemap 7286 ltsopi 7349 recexnq 7419 ltsonq 7427 ltaddnq 7436 nsmallnqq 7441 ltpopr 7624 ltposr 7792 1idsr 7797 00sr 7798 axltirr 8054 leid 8071 reapirr 8564 inelr 8571 apsqgt0 8588 apirr 8592 msqge0 8603 recextlem1 8638 recexaplem2 8639 recexap 8640 div1 8690 cju 8948 2halves 9178 msqznn 9383 xrltnr 9809 xrleid 9830 iooidg 9939 iccid 9955 m1expeven 10598 expubnd 10608 sqneg 10610 sqcl 10612 sqap0 10618 nnsqcl 10621 qsqcl 10623 subsq2 10659 bernneq 10672 faclbnd 10753 faclbnd3 10755 cjmulval 10929 sin2t 11789 cos2t 11790 gcd0id 12012 lcmid 12112 lcmgcdeq 12115 intopsn 12843 mgm1 12846 sgrp1 12874 mnd1 12907 mnd1id 12908 grpsubid 13028 grp1 13050 grp1inv 13051 ringadd2 13381 ring1 13411 idcn 14172 ismet 14304 isxmet 14305 resubmet 14508 bj-snexg 15125 |
Copyright terms: Public domain | W3C validator |