![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anidm | Unicode version |
Description: Idempotent law for conjunction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
Ref | Expression |
---|---|
anidm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.24 388 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 131 |
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 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anidmdbi 391 anandi 558 anandir 559 truantru 1338 falanfal 1341 truxortru 1356 truxorfal 1357 falxortru 1358 falxorfal 1359 sbnf2 1906 2eu4 2042 inidm 3210 ralidm 3386 opcom 4086 opeqsn 4088 poirr 4143 rnxpid 4878 xp11m 4882 fununi 5095 brprcneu 5311 erinxp 6380 dom2lem 6543 dmaddpi 6945 dmmulpi 6946 enq0ref 7053 enq0tr 7054 expap0 10046 sqap0 10082 gcddvds 11294 |
Copyright terms: Public domain | W3C validator |