![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anidm | Structured version Visualization version GIF version |
Description: Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
Ref | Expression |
---|---|
anidm | ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.24 553 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
2 | 1 | bicomi 214 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 383 |
This theorem is referenced by: anidmdbi 555 anandi 655 anandir 656 nannot 1601 truantru 1654 falanfal 1657 nic-axALT 1747 inidm 3971 opcom 5092 opeqsnOLD 5096 poirr 5181 asymref2 5654 xp11 5710 fununi 6104 brprcneu 6325 f13dfv 6673 erinxp 7973 dom2lem 8149 pssnn 8334 dmaddpi 9914 dmmulpi 9915 gcddvds 15433 iscatd2 16549 dfiso2 16639 isnsg2 17832 eqger 17852 gaorber 17948 efgcpbllemb 18375 xmeter 22458 caucfil 23300 tgcgr4 25647 axcontlem5 26069 cplgr3v 26566 erclwwlkref 27170 clwwlkn2 27200 erclwwlknref 27227 frgr3v 27457 numclwlk1lem1 27560 disjunsn 29745 bnj594 31320 subfaclefac 31496 isbasisrelowllem1 33540 isbasisrelowllem2 33541 inixp 33855 opideq 34452 cdlemg33b 36516 eelT11 39457 uunT11 39548 uunT11p1 39549 uunT11p2 39550 uun111 39557 2reu4a 41709 |
Copyright terms: Public domain | W3C validator |