Theorem anidm 111

Description: Idempotent law.

Assertion

Ref	Expression
anidm	(a ^ a) = a

Proof of Theorem anidm

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

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

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 1040  lem3.3.7i1e2 1060  lem3.4.3 1075  lem4.6.2e1 1079

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

Copyright terms: Public domain