Theorem an0r 109

Description: Conjunction with 0.

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 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 1065

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

Copyright terms: Public domain