Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anidm | GIF 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 387 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
2 | 1 | bicomi 130 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: anidmdbi 390 anandi 554 anandir 555 truantru 1332 falanfal 1335 truxortru 1350 truxorfal 1351 falxortru 1352 falxorfal 1353 sbnf2 1898 2eu4 2034 inidm 3175 ralidm 3341 opcom 4005 opeqsn 4007 poirr 4062 rnxpid 4775 xp11m 4779 fununi 4987 brprcneu 5191 erinxp 6203 dom2lem 6275 dmaddpi 6515 dmmulpi 6516 enq0ref 6623 enq0tr 6624 expap0 9506 sqap0 9542 gcddvds 10355 |
Copyright terms: Public domain | W3C validator |