|   | 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 563 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
| 2 | 1 | bicomi 224 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 | 
| 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 207 df-an 396 | 
| This theorem is referenced by: anidmdbi 565 anandi 676 anandir 677 3anidm 1103 truantru 1572 falanfal 1575 nic-axALT 1673 inidm 4226 2reu4lem 4521 opcom 5505 poirr 5603 asymref2 6136 xp11 6194 fununi 6640 brprcneu 6895 brprcneuALT 6896 f13dfv 7295 erinxp 8832 dom2lem 9033 pssnn 9209 djuinf 10230 dmaddpi 10931 dmmulpi 10932 gcddvds 16541 iscatd2 17725 dfiso2 17817 isnsg2 19175 eqger 19197 gaorber 19327 efgcpbllemb 19774 xmeter 24444 caucfil 25318 tgcgr4 28540 axcontlem5 28984 cplgr3v 29453 erclwwlkref 30040 clwwlkn2 30064 erclwwlknref 30089 frgr3v 30295 numclwlk1lem1 30389 disjunsn 32608 bnj594 34927 subfaclefac 35182 isbasisrelowllem1 37357 isbasisrelowllem2 37358 inixp 37736 opideq 38345 cdlemg33b 40710 eelT11 44732 uunT11 44821 uunT11p1 44822 uunT11p2 44823 uun111 44830 | 
| Copyright terms: Public domain | W3C validator |