Theorem an0r 109

Description: Conjunction with 0. (Contributed by NM, 26-Nov-1997.)

Assertion

Ref	Expression
an0r	(0 ∩ a) = 0

Proof of Theorem an0r

Step	Hyp	Ref	Expression
1		ancom 74	. 2 (0 ∩ a) = (a ∩ 0)
2		an0 108	. 2 (a ∩ 0) = 0
3	1, 2	ax-r2 36	1 (0 ∩ a) = 0

Syntax hints:   = wb 1   ∩ wa 7  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:  ud3lem1a  566  ud3lem3b  573  ud5lem1b  587  ud5lem3a  591  ud5lem3b  592  bi3  839  bi4  840  mlaconj4  844  comanblem2  871  marsdenlem3  882  mhcor1  888  govar  896  lem3.3.7i3e1  1066