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 585 anandir 586 truantru 1396 falanfal 1399 truxortru 1414 truxorfal 1415 falxortru 1416 falxorfal 1417 sbnf2 1974 2eu4 2112 inidm 3336 ralidm 3515 opcom 4235 opeqsn 4237 poirr 4292 rnxpid 5045 xp11m 5049 fununi 5266 brprcneu 5489 erinxp 6587 dom2lem 6750 dmaddpi 7287 dmmulpi 7288 enq0ref 7395 enq0tr 7396 expap0 10506 sqap0 10542 xrmaxiflemcom 11212 gcddvds 11918 xmeter 13230 |
Copyright terms: Public domain | W3C validator |