Theorem a5b 120

Description: Absorption law.

Assertion

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

Proof of Theorem a5b

Step	Hyp	Ref	Expression
1		df-a 40	. . 3 (a ^ b) = (a' v b')'
2	1	lor 70	. 2 (a v (a ^ b)) = (a v (a' v b')')
3		ax-a5 34	. 2 (a v (a' v b')') = a
4	2, 3	ax-r2 36	1 (a v (a ^ b)) = a

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

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 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem4.6.2e1 1079

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

Copyright terms: Public domain