![]() |
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 3345 ralidm 3524 opcom 4251 opeqsn 4253 poirr 4308 rnxpid 5064 xp11m 5068 fununi 5285 brprcneu 5509 erinxp 6609 dom2lem 6772 dmaddpi 7324 dmmulpi 7325 enq0ref 7432 enq0tr 7433 expap0 10550 sqap0 10587 xrmaxiflemcom 11257 gcddvds 11964 isnsg2 13063 eqger 13083 xmeter 13939 |
Copyright terms: Public domain | W3C validator |