Theorem an0r 101

Description: Conjunction with 0.

Assertion

Ref	Expression
an0r	(0 ∩ a) = 0

Proof of Theorem an0r

Step	Hyp	Ref	Expression
1		ancom 68	. 2 (0 ∩ a) = (a ∩ 0)
2		an0 100	. 2 (a ∩ 0) = 0
3	1, 2	ax-r2 35	1 (0 ∩ a) = 0

Syntax hints:   = wb 1   ∩ wa 7  0wf 10

This theorem is referenced by:  ud3lem1a 548  ud3lem3b 555  ud5lem1b 569  ud5lem3a 573  ud5lem3b 574  bi3 821  bi4 822  mlaconj4 826  comanblem2 853  marsdenlem3 864  mhcor1 870  govar 876

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a4 32  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

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

metamath.org