Theorem or0r 103

Description: Disjunction with 0.

Assertion

Ref	Expression
or0r	(0 v a) = a

Proof of Theorem or0r

Step	Hyp	Ref	Expression
1		ax-a2 31	. 2 (0 v a) = (a v 0)
2		or0 102	. 2 (a v 0) = a
3	1, 2	ax-r2 36	1 (0 v a) = a

Syntax hints:   = wb 1   v wo 6  0wf 9

This theorem is referenced by:  k1-4 359  ud3lem1a 566  ud3lem1d 569  ud5lem1b 587  bi1o1a 798  bi3 839  bi4 840  mlaconj4 844  mhlemlem1 874  mhlem1 877  marsdenlem2 881  mlaconjo 886  mhcor1 888  e2astlem1 895  oa6v4v 933  lem3.3.4 1052  lem3.3.7i3e1 1065

This theorem was proved from axioms:  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

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

Copyright terms: Public domain