![]() |
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 676 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
2 | 1 | bicomi 214 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 |
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 385 |
This theorem is referenced by: anidmdbi 679 anandi 888 anandir 889 nannot 1493 truantru 1546 falanfal 1549 nic-axALT 1639 inidm 3855 opcom 4994 opeqsn 4996 poirr 5075 asymref2 5548 xp11 5604 fununi 6002 brprcneu 6222 f13dfv 6570 erinxp 7864 dom2lem 8037 pssnn 8219 dmaddpi 9750 dmmulpi 9751 gcddvds 15272 iscatd2 16389 dfiso2 16479 isnsg2 17671 eqger 17691 gaorber 17787 efgcpbllemb 18214 xmeter 22285 caucfil 23127 tgcgr4 25471 axcontlem5 25893 cplgr3v 26387 erclwwlkref 26977 clwwlkn2 27007 erclwwlknref 27033 frgr3v 27255 disjunsn 29533 bnj594 31108 subfaclefac 31284 isbasisrelowllem1 33333 isbasisrelowllem2 33334 inixp 33653 opideq 34250 cdlemg33b 36312 eelT11 39249 uunT11 39340 uunT11p1 39341 uunT11p2 39342 uun111 39349 2reu4a 41510 |
Copyright terms: Public domain | W3C validator |