Theorem oridm 104

Description: Idempotent law.

Assertion

Ref	Expression
oridm	(a v a) = a

Proof of Theorem oridm

Step	Hyp	Ref	Expression
1		ax-a1 30	. . . 4 a = a''
2		or0 96	. . . . . 6 (a' v 0) = a'
3	2	ax-r1 35	. . . . 5 a' = (a' v 0)
4	3	ax-r4 37	. . . 4 a'' = (a' v 0)'
5	1, 4	ax-r2 36	. . 3 a = (a' v 0)'
6	5	lor 67	. 2 (a v a) = (a v (a' v 0)')
7		ax-a5 34	. 2 (a v (a' v 0)') = a
8	6, 7	ax-r2 36	1 (a v a) = a

Syntax hints:   = wb 1  'wn 4   v wo 6  0wf 9

This theorem is referenced by:  anidm 105  orordi 106  orordir 107  omlem1 121  bile 136  lel2or 164  ler2or 166  ledi 168  ledio 170  comid 181  ska15 238  wql1 287  womle2a 289  wbile 387  wledi 391  wledio 392  ka4ot 421  lem3a.1 430  i3bi 482  dfi3b 485  lem4 497  binr3 505  i3abs1 508  i3th5 533  ud1lem3 548  ud4lem2 568  ud5lem3 580  u1lemona 611  u2lemob 617  u3lemob 618  u4lemob 619  u4lem4 745  u5lem4 746  u3lem6 753  u4lem6 754  u5lem6 755  u3lem9 770  biao 785  3vth5 794  3vth6 795  3vth9 798  3vded21 803  3vded22 804  3vroa 817  oau 915  oa23 922  distoa 930  oa3-2lema 964  oa3-2lemb 965  oa3-5lem 970  d3oa 981  oagen1 1000  oadistd 1009  4oagen1 1027  4oadist 1029

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-t 41  df-f 42

Copyright terms: Public domain