![]() |
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 113 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm2.43i 48 |
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-ia3 106 |
This theorem is referenced by: sylancb 409 sylancbr 410 intsng 3722 pwnss 3994 posng 4510 xpid11m 4658 resiexg 4757 f1mpt 5550 f1eqcocnv 5570 isopolem 5601 poxp 5997 nnmsucr 6249 erex 6314 ecopover 6388 ecopoverg 6391 enrefg 6479 3xpfi 6639 ltsopi 6877 recexnq 6947 ltsonq 6955 ltaddnq 6964 nsmallnqq 6969 ltpopr 7152 ltposr 7307 1idsr 7312 00sr 7313 axltirr 7551 leid 7567 reapirr 8052 inelr 8059 apsqgt0 8076 apirr 8080 msqge0 8091 recextlem1 8118 recexaplem2 8119 recexap 8120 div1 8168 cju 8419 2halves 8643 msqznn 8844 xrltnr 9248 xrleid 9267 iooidg 9325 iccid 9341 m1expeven 9998 expubnd 10008 sqneg 10010 sqcl 10012 sqap0 10017 nnsqcl 10020 qsqcl 10022 subsq2 10058 bernneq 10070 faclbnd 10145 faclbnd3 10147 cjmulval 10318 sin2t 11036 cos2t 11037 gcd0id 11244 lcmid 11336 lcmgcdeq 11339 bj-snexg 11758 |
Copyright terms: Public domain | W3C validator |