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 393 | . 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 396 anandi 580 anandir 581 truantru 1383 falanfal 1386 truxortru 1401 truxorfal 1402 falxortru 1403 falxorfal 1404 sbnf2 1961 2eu4 2099 inidm 3317 ralidm 3495 opcom 4213 opeqsn 4215 poirr 4270 rnxpid 5023 xp11m 5027 fununi 5241 brprcneu 5464 erinxp 6557 dom2lem 6720 dmaddpi 7248 dmmulpi 7249 enq0ref 7356 enq0tr 7357 expap0 10459 sqap0 10495 xrmaxiflemcom 11158 gcddvds 11863 xmeter 12932 |
Copyright terms: Public domain | W3C validator |