![]() |
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 1380 falanfal 1383 truxortru 1398 truxorfal 1399 falxortru 1400 falxorfal 1401 sbnf2 1957 2eu4 2093 inidm 3290 ralidm 3468 opcom 4180 opeqsn 4182 poirr 4237 rnxpid 4981 xp11m 4985 fununi 5199 brprcneu 5422 erinxp 6511 dom2lem 6674 dmaddpi 7157 dmmulpi 7158 enq0ref 7265 enq0tr 7266 expap0 10354 sqap0 10390 xrmaxiflemcom 11050 gcddvds 11688 xmeter 12644 |
Copyright terms: Public domain | W3C validator |