Theorem anidm 111

Description: Idempotent law. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
anidm	(a ∩ a) = a

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ∩ a) = (a⊥ ∪ a⊥ )⊥
2		oridm 110	. . 3 (a⊥ ∪ a⊥ ) = a⊥
3	2	con2 67	. 2 (a⊥ ∪ a⊥ )⊥ = a
4	1, 3	ax-r2 36	1 (a ∩ a) = a

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42

This theorem is referenced by:  anandi  114  anandir  115  biid  116  mi  125  lel2an  171  ler2an  173  ledi  174  ledio  176  i3id  251  i1id  275  i2id  276  nom11  308  nom14  311  nom15  312  nom21  314  nom24  317  nom25  318  wdf-c2  384  wledi  405  wledio  406  wlem14  430  oml4  487  i3bi  496  dfi3b  499  i3lem1  504  ud2lem2  564  ud3lem1b  567  ud3lem2  571  ud5lem1a  586  ud5lem1c  588  ud5lem2  590  ud5lem3a  591  ud5lem3c  593  u1lemaa  600  u3lemaa  602  u4lemaa  603  u5lemaa  604  u2lemana  606  u4lemana  608  u5lemana  609  u1lemab  610  u3lemab  612  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u1lemle2  715  u4lemle2  718  u5lemle2  719  oi3oa3lem1  732  u1lem2  744  u2lem2  745  u1lem4  757  u4lem6  768  u3lem10  785  u3lem11  786  test2  803  3vth7  810  1oa  820  1oaiii  823  2oalem1  825  2oath1  826  oale  829  bi3  839  bi4  840  mlaconj4  844  comanblem2  871  oaidlem2  931  oaidlem2g  932  oa6v4v  933  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oaliii  1001  oath1  1004  oalem1  1005  oadist  1019  4oath1  1041  lem3.3.7i1e2  1061  lem3.4.3  1076  lem4.6.2e1  1082