Theorem an0 108

Description: Conjunction with 0. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
an0	(a ∩ 0) = 0

Proof of Theorem an0

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ∩ 0) = (a⊥ ∪ 0⊥ )⊥
2		or1 104	. . . 4 (a⊥ ∪ 1) = 1
3		df-f 42	. . . . . 6 0 = 1⊥
4	3	con2 67	. . . . 5 0⊥ = 1
5	4	lor 70	. . . 4 (a⊥ ∪ 0⊥ ) = (a⊥ ∪ 1)
6	2, 5, 4	3tr1 63	. . 3 (a⊥ ∪ 0⊥ ) = 0⊥
7	6	con2 67	. 2 (a⊥ ∪ 0⊥ )⊥ = 0
8	1, 7	ax-r2 36	1 (a ∩ 0) = 0

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a4 33  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-t 41  df-f 42

This theorem is referenced by:  an0r  109  1b  117  comm0  178  wwfh1  216  wwfh2  217  ska8  236  wfh1  423  wfh2  424  fh1  469  fh2  470  oml4  487  gsth  489  i3bi  496  lem4  511  ud3lem1a  566  ud3lem2  571  ud3lem3b  573  ud4lem1a  577  ud4lem1b  578  ud4lem2  582  ud5lem1a  586  ud5lem1b  587  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u3lemanb  617  u4lemanb  618  u5lemanb  619  u2lemle2  716  u4lemle2  718  u5lemle2  719  u5lembi  725  u4lem6  768  u2lem8  782  u3lem13b  790  3vded21  817  mlalem  832  bi3  839  bi4  840  comanblem1  870  marsdenlem3  882  marsdenlem4  883  mlaconjo  886  mhcor1  888  oa3-2lema  978  oa3-1lem  982  oa3-2to2s  990