Theorem a5c 113

Description: Absorption law.

Assertion

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

Proof of Theorem a5c

Step	Hyp	Ref	Expression
1		ax-a1 29	. . . . 5 a = a⊥ ⊥
2	1	ax-r5 37	. . . 4 (a ∪ b) = (a⊥ ⊥ ∪ b)
3	2	lan 70	. . 3 (a ∩ (a ∪ b)) = (a ∩ (a⊥ ⊥ ∪ b))
4		df-a 39	. . 3 (a ∩ (a⊥ ⊥ ∪ b)) = (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥
5	3, 4	ax-r2 35	. 2 (a ∩ (a ∪ b)) = (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥
6		ax-a5 33	. . 3 (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ ) = a⊥
7	6	con2 64	. 2 (a⊥ ∪ (a⊥ ⊥ ∪ b)⊥ )⊥ = a
8	5, 7	ax-r2 35	1 (a ∩ (a ∪ b)) = a

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem is referenced by:  leoa 115  mi 117  letr 129  leo 150  wa5c 193  wwcom3ii 207  ska7 227  nom15 304  nom22 307  nom23 308  nom25 310  2vwomlem 347  wcomlem 364  wdf-c2 366  wletr 378  wcom3ii 401  oml5a 432  comcom 435  com3ii 439  i3lem1 486  i3orlem3 536  ud3lem1a 548  ud3lem1b 549  ud3lem1d 551  ud3lem2 553  ud4lem1d 562  ud4lem2 564  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  ud5lem3 576  u1lemana 587  u2lemab 593  u3lemab 594  u5lembi 707  u24lem 752  u3lem15 777  i2i1i1 782  3vded21 799  salem1 819  neg3antlem2 847  mhlemlem1 856  mhlem1 859  gomaex3lem2 895  oath1 984  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

metamath.org