![]() |
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 375 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 123 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: anidmdbi 378 anandi 524 anandir 525 truantru 1289 falanfal 1292 truxortru 1307 truxorfal 1308 falxortru 1309 falxorfal 1310 sbnf2 1854 2eu4 1990 inidm 3140 ralidm 3315 opcom 3978 opeqsn 3980 poirr 4035 rnxpid 4698 xp11m 4702 fununi 4910 brprcneu 5114 erinxp 6116 dom2lem 6188 dmaddpi 6309 dmmulpi 6310 enq0ref 6416 enq0tr 6417 expap0 8939 |
Copyright terms: Public domain | W3C validator |