Theorem a5c 121

Description: Absorption law.

Assertion

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

Proof of Theorem a5c

Step	Hyp	Ref	Expression
1		ax-a1 30	. . . . 5 a = a''
2	1	ax-r5 38	. . . 4 (a v b) = (a'' v b)
3	2	lan 77	. . 3 (a ^ (a v b)) = (a ^ (a'' v b))
4		df-a 40	. . 3 (a ^ (a'' v b)) = (a' v (a'' v b)')'
5	3, 4	ax-r2 36	. 2 (a ^ (a v b)) = (a' v (a'' v b)')'
6		ax-a5 34	. . 3 (a' v (a'' v b)') = a'
7	6	con2 67	. 2 (a' v (a'' v b)')' = a
8	5, 7	ax-r2 36	1 (a ^ (a v b)) = a

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

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 1040  lem3.3.4 1052

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

Copyright terms: Public domain