Theorem orabs 120

Description: Absorption law. (Contributed by NM, 11-Aug-1997.)

Assertion

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

Proof of Theorem orabs

Step	Hyp	Ref	Expression
1		df-a 40	. . 3 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
2	1	lor 70	. 2 (a ∪ (a ∩ b)) = (a ∪ (a⊥ ∪ b⊥ )⊥ )
3		ax-a5 34	. 2 (a ∪ (a⊥ ∪ b⊥ )⊥ ) = a
4	2, 3	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-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r5 38

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  leao  124  omlem1  127  lea  160  lecom  180  wa5b  200  nom12  309  nom13  310  wcomlem  382  wlecom  409  oml5  449  comcom  453  i3lem3  506  lem4  511  i3abs1  522  i3th1  543  i3con  551  ud1lem1  560  ud2lem3  565  ud3lem1  570  ud3lem3c  574  ud5lem3  594  u5lemaa  604  u5lemoa  624  u12lem  771  u3lem7  774  u1lem11  780  u3lem10  785  i1abs  801  test  802  3vded3  819  1oaii  824  sa5  836  neg3antlem2  865  gomaex3lem3  916  oau  929  oa23  936  oa3-6lem  980  oalii  1002  oalem2  1006  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem4.6.2e1  1082  dp15lemd  1157  xdp15  1199  xxdp15  1202  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208