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 392 | . 2 | |
2 | 1 | bicomi 131 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anidmdbi 395 anandi 579 anandir 580 truantru 1379 falanfal 1382 truxortru 1397 truxorfal 1398 falxortru 1399 falxorfal 1400 sbnf2 1954 2eu4 2090 inidm 3280 ralidm 3458 opcom 4167 opeqsn 4169 poirr 4224 rnxpid 4968 xp11m 4972 fununi 5186 brprcneu 5407 erinxp 6496 dom2lem 6659 dmaddpi 7126 dmmulpi 7127 enq0ref 7234 enq0tr 7235 expap0 10316 sqap0 10352 xrmaxiflemcom 11011 gcddvds 11641 xmeter 12594 |
Copyright terms: Public domain | W3C validator |