Theorem anabs 121

Description: Absorption law.

Assertion

Ref	Expression
anabs	(a ∩ (a ∪ b)) = a

Proof of Theorem anabs

Step	Hyp	Ref	Expression
1		ax-a1 30	. . . . 5 a = a⊥ ⊥
2	1	ax-r5 38	. . . 4 (a ∪ b) = (a⊥ ⊥ ∪ b)
3	2	lan 77	. . 3 (a ∩ (a ∪ b)) = (a ∩ (a⊥ ⊥ ∪ b))
4		df-a 40	. . 3 (a ∩ (a⊥ ⊥ ∪ b)) = (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥
5	3, 4	ax-r2 36	. 2 (a ∩ (a ∪ b)) = (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥
6		ax-a5 34	. . 3 (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ ) = a⊥
7	6	con2 67	. 2 (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥ = a
8	5, 7	ax-r2 36	1 (a ∩ (a ∪ b)) = 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

This theorem is referenced by:  leoa  123  mi  125  letr  137  leo  158  wa5c  201  wwcom3ii  215  ska7  235  nom15  312  nom22  315  nom23  316  nom25  318  k1-6  353  k1-7  354  2vwomlem  365  wcomlem  382  wdf-c2  384  wletr  396  wcom3ii  419  oml5a  450  comcom  453  com3ii  457  i3lem1  504  i3orlem3  554  ud3lem1a  566  ud3lem1b  567  ud3lem1d  569  ud3lem2  571  ud4lem1d  580  ud4lem2  582  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  ud5lem3c  593  ud5lem3  594  u1lemana  605  u2lemab  611  u3lemab  612  u5lembi  725  u24lem  770  u3lem15  795  i2i1i1  800  3vded21  817  salem1  837  neg3antlem2  865  mhlemlem1  874  mhlem1  877  gomaex3lem2  915  oath1  1004  4oath1  1041  lem3.3.4  1053  modexp  1150  dp53lemb  1162  dp35lemb  1174  xdp53  1198  xxdp53  1201  xdp43lem  1203  xdp43  1205  3dp43  1206