Theorem an0 100

Description: Conjunction with 0.

Assertion

Ref	Expression
an0	(a ^ 0) = 0

Proof of Theorem an0

Step	Hyp	Ref	Expression
1		df-a 39	. 2 (a ^ 0) = (a_|_ v 0_|_)_|_
2		or1 96	. . . 4 (a_|_ v 1) = 1
3		df-f 41	. . . . . 6 0 = 1_|_
4	3	con2 64	. . . . 5 0_|_ = 1
5	4	lor 66	. . . 4 (a_|_ v 0_|_) = (a_|_ v 1)
6	2, 5, 4	3tr1 60	. . 3 (a_|_ v 0_|_) = 0_|_
7	6	con2 64	. 2 (a_|_ v 0_|_)_|_ = 0
8	1, 7	ax-r2 35	1 (a ^ 0) = 0

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9  0wf 10

This theorem is referenced by:  an0r 101  1b 109  comm0 170  wwfh1 208  wwfh2 209  ska8 228  wfh1 405  wfh2 406  fh1 451  fh2 452  oml4 469  gsth 471  i3bi 478  lem4 493  ud3lem1a 548  ud3lem2 553  ud3lem3b 555  ud4lem1a 559  ud4lem1b 560  ud4lem2 564  ud5lem1a 568  ud5lem1b 569  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u3lemanb 599  u4lemanb 600  u5lemanb 601  u2lemle2 698  u4lemle2 700  u5lemle2 701  u5lembi 707  u4lem6 750  u2lem8 764  u3lem13b 772  3vded21 799  mlalem 814  bi3 821  bi4 822  comanblem1 852  marsdenlem3 864  marsdenlem4 865  mlaconjo 868  mhcor1 870  oa3-2lema 958  oa3-1lem 962  oa3-2to2s 970

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