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 392 | . 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 395 anandi 564 anandir 565 truantru 1364 falanfal 1367 truxortru 1382 truxorfal 1383 falxortru 1384 falxorfal 1385 sbnf2 1934 2eu4 2070 inidm 3255 ralidm 3433 opcom 4142 opeqsn 4144 poirr 4199 rnxpid 4943 xp11m 4947 fununi 5161 brprcneu 5382 erinxp 6471 dom2lem 6634 dmaddpi 7101 dmmulpi 7102 enq0ref 7209 enq0tr 7210 expap0 10291 sqap0 10327 xrmaxiflemcom 10986 gcddvds 11579 xmeter 12532 |
Copyright terms: Public domain | W3C validator |