![]() |
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 395 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
2 | 1 | bicomi 132 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 |
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 1401 falanfal 1404 truxortru 1419 truxorfal 1420 falxortru 1421 falxorfal 1422 sbnf2 1981 2eu4 2119 inidm 3344 ralidm 3523 opcom 4250 opeqsn 4252 poirr 4307 rnxpid 5063 xp11m 5067 fununi 5284 brprcneu 5508 erinxp 6608 dom2lem 6771 dmaddpi 7323 dmmulpi 7324 enq0ref 7431 enq0tr 7432 expap0 10549 sqap0 10586 xrmaxiflemcom 11256 gcddvds 11963 isnsg2 13061 eqger 13081 xmeter 13906 |
Copyright terms: Public domain | W3C validator |