![]() |
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 395 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 132 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: anidmdbi 398 anandi 590 anandir 591 truantru 1412 falanfal 1415 truxortru 1430 truxorfal 1431 falxortru 1432 falxorfal 1433 sbnf2 1993 2eu4 2131 inidm 3359 ralidm 3538 opcom 4268 opeqsn 4270 poirr 4325 rnxpid 5081 xp11m 5085 fununi 5303 brprcneu 5527 erinxp 6635 dom2lem 6798 dmaddpi 7354 dmmulpi 7355 enq0ref 7462 enq0tr 7463 expap0 10581 sqap0 10618 xrmaxiflemcom 11289 gcddvds 11996 isnsg2 13142 eqger 13163 xmeter 14393 |
Copyright terms: Public domain | W3C validator |