Theorem a5b 112

Description: Absorption law.

Assertion

Ref	Expression
a5b	(a v (a ^ b)) = a

Proof of Theorem a5b

Step	Hyp	Ref	Expression
1		df-a 39	. . 3 (a ^ b) = (a_|_ v b_|_)_|_
2	1	lor 66	. 2 (a v (a ^ b)) = (a v (a_|_ v b_|_)_|_)
3		ax-a5 33	. 2 (a v (a_|_ v b_|_)_|_) = a
4	2, 3	ax-r2 35	1 (a v (a ^ b)) = a

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  leao 116  omlem1 119  lea 152  lecom 172  wa5b 192  nom12 301  nom13 302  wcomlem 364  wlecom 391  oml5 431  comcom 435  i3lem3 488  lem4 493  i3abs1 504  i3th1 525  i3con 533  ud1lem1 542  ud2lem3 547  ud3lem1 552  ud3lem3c 556  ud5lem3 576  u5lemaa 586  u5lemoa 606  u12lem 753  u3lem7 756  u1lem11 762  u3lem10 767  i1abs 783  test 784  3vded3 801  1oaii 806  sa5 818  neg3antlem2 847  gomaex3lem3 896  oau 909  oa23 916  oa3-6lem 960  oalii 982  oalem2 986

This theorem was proved from axioms:  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-a 39

metamath.org