Theorem or0 94

Description: Disjunction with 0.

Assertion

Ref	Expression
or0	(a v 0) = a

Proof of Theorem or0

Step	Hyp	Ref	Expression
1		dff2 92	. . . 4 0 = (a v a_|_)_|_
2		ax-a2 30	. . . . 5 (a v a_|_) = (a_|_ v a)
3	2	ax-r4 36	. . . 4 (a v a_|_)_|_ = (a_|_ v a)_|_
4	1, 3	ax-r2 35	. . 3 0 = (a_|_ v a)_|_
5	4	lor 66	. 2 (a v 0) = (a v (a_|_ v a)_|_)
6		ax-a5 33	. 2 (a v (a_|_ v a)_|_) = a
7	5, 6	ax-r2 35	1 (a v 0) = a

Syntax hints:   = wb 1  _|_wn 4   v wo 6  0wf 10

This theorem is referenced by:  or0r 95  an1 98  oridm 102  1b 109  le0 139  comm0 170  wwoml3 205  skr0 234  i3id 243  1i1 266  2vwomlem 347  wom5 363  wle0 372  oml3 434  oml4 469  gsth 471  i3bi 478  lem4 493  i3abs3 506  ud2lem1 545  ud3lem1a 548  ud3lem1b 549  ud3lem1 552  ud3lem2 553  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1d 562  ud4lem2 564  ud4lem3 567  ud5lem1a 568  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u3lemc4 685  u4lemc4 686  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u5lembi 707  u1lemn1b 712  u2lem1 717  u4lem4 741  u2lem5 744  u4lem5 746  u4lem6 750  u2lem8 764  u3lem11 768  u3lem13a 771  u3lem13b 772  u3lem15 777  3vded21 799  3vded3 801  1oa 802  2oath1 808  bi3 821  bi4 822  mlaconj4 826  neg3antlem2 847  comanblem1 852  comanblem2 853  mhlem 858  mhlem1 859  marsdenlem3 864  marsdenlem4 865  mlaconjo 868  mhcor1 870  govar 876  oa6v4v 913  oa3-2lema 958  oa3-1lem 962  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970

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

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

metamath.org