![]() |
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 3876 pwnss 4156 posng 4694 sqxpexg 4738 xpid11 4845 resiexg 4947 f1mpt 5765 f1eqcocnv 5785 isopolem 5816 poxp 6226 nnmsucr 6482 erex 6552 ecopover 6626 ecopoverg 6629 enrefg 6757 3xpfi 6923 ltsopi 7297 recexnq 7367 ltsonq 7375 ltaddnq 7384 nsmallnqq 7389 ltpopr 7572 ltposr 7740 1idsr 7745 00sr 7746 axltirr 8001 leid 8018 reapirr 8511 inelr 8518 apsqgt0 8535 apirr 8539 msqge0 8550 recextlem1 8584 recexaplem2 8585 recexap 8586 div1 8636 cju 8894 2halves 9124 msqznn 9329 xrltnr 9753 xrleid 9774 iooidg 9883 iccid 9899 m1expeven 10540 expubnd 10550 sqneg 10552 sqcl 10554 sqap0 10559 nnsqcl 10562 qsqcl 10564 subsq2 10600 bernneq 10613 faclbnd 10692 faclbnd3 10694 cjmulval 10868 sin2t 11728 cos2t 11729 gcd0id 11950 lcmid 12050 lcmgcdeq 12053 intopsn 12665 mgm1 12668 sgrp1 12695 mnd1 12724 mnd1id 12725 grpsubid 12830 grp1 12852 grp1inv 12853 ringadd2 13023 ring1 13049 idcn 13345 ismet 13477 isxmet 13478 resubmet 13681 bj-snexg 14286 |
Copyright terms: Public domain | W3C validator |