Theorem anidm 103

Description: Idempotent law.

Assertion

Ref	Expression
anidm	(a ^ a) = a

Proof of Theorem anidm

Step	Hyp	Ref	Expression
1		df-a 39	. 2 (a ^ a) = (a_|_ v a_|_)_|_
2		oridm 102	. . 3 (a_|_ v a_|_) = a_|_
3	2	con2 64	. 2 (a_|_ v a_|_)_|_ = a
4	1, 3	ax-r2 35	1 (a ^ a) = a

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  anandi 106  anandir 107  biid 108  mi 117  lel2an 163  ler2an 165  ledi 166  ledio 168  i3id 243  i1id 267  i2id 268  nom11 300  nom14 303  nom15 304  nom21 306  nom24 309  nom25 310  wdf-c2 366  wledi 387  wledio 388  wlem14 412  oml4 469  i3bi 478  dfi3b 481  i3lem1 486  ud2lem2 546  ud3lem1b 549  ud3lem2 553  ud5lem1a 568  ud5lem1c 570  ud5lem2 572  ud5lem3a 573  ud5lem3c 575  u1lemaa 582  u3lemaa 584  u4lemaa 585  u5lemaa 586  u2lemana 588  u4lemana 590  u5lemana 591  u1lemab 592  u3lemab 594  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u1lemle2 697  u4lemle2 700  u5lemle2 701  oi3oa3lem1 714  u1lem2 726  u2lem2 727  u1lem4 739  u4lem6 750  u3lem10 767  u3lem11 768  test2 785  3vth7 792  1oa 802  1oaiii 805  2oalem1 807  2oath1 808  oale 811  bi3 821  bi4 822  mlaconj4 826  comanblem2 853  oaidlem2 911  oaidlem2g 912  oa6v4v 913  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oaliii 981  oath1 984  oalem1 985  oadist 999  4oath1 1020

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

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

metamath.org