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 673 | . 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | |
2 | 1 | bicomi 213 | 1 ⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: anidmdbi 676 anandi 867 anandir 868 nannot 1445 truantru 1497 falanfal 1500 nic-axALT 1590 inidm 3784 opcom 4890 opeqsn 4892 poirr 4970 asymref2 5432 xp11 5488 fununi 5878 brprcneu 6096 f13dfv 6430 erinxp 7708 dom2lem 7881 pssnn 8063 dmaddpi 9591 dmmulpi 9592 gcddvds 15063 iscatd2 16165 dfiso2 16255 isnsg2 17447 eqger 17467 gaorber 17564 efgcpbllemb 17991 xmeter 22048 caucfil 22889 tgcgr4 25226 axcontlem5 25648 cusgra2v 25991 cusgra3v 25993 erclwwlkref 26341 erclwwlknref 26353 frgra3v 26529 disjunsn 28789 bnj594 30236 subfaclefac 30412 isbasisrelowllem1 32379 isbasisrelowllem2 32380 inixp 32693 cdlemg33b 35013 eelT11 37953 uunT11 38044 uunT11p1 38045 uunT11p2 38046 uun111 38053 2reu4a 39838 cplgr3v 40657 clwwlksn2 41217 erclwwlksref 41241 erclwwlksnref 41253 frgr3v 41445 |
Copyright terms: Public domain | W3C validator |