Theorem an0 108

Description: Conjunction with 0.

Assertion

Ref	Expression
an0	(a ^ 0) = 0

Proof of Theorem an0

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ^ 0) = (a' v 0')'
2		or1 104	. . . 4 (a' v 1) = 1
3		df-f 42	. . . . . 6 0 = 1'
4	3	con2 67	. . . . 5 0' = 1
5	4	lor 70	. . . 4 (a' v 0') = (a' v 1)
6	2, 5, 4	3tr1 63	. . 3 (a' v 0') = 0'
7	6	con2 67	. 2 (a' v 0')' = 0
8	1, 7	ax-r2 36	1 (a ^ 0) = 0

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9

This theorem is referenced by:  an0r 109  1b 117  comm0 178  wwfh1 216  wwfh2 217  ska8 236  wfh1 423  wfh2 424  fh1 469  fh2 470  oml4 487  gsth 489  i3bi 496  lem4 511  ud3lem1a 566  ud3lem2 571  ud3lem3b 573  ud4lem1a 577  ud4lem1b 578  ud4lem2 582  ud5lem1a 586  ud5lem1b 587  ud5lem2 590  ud5lem3a 591  ud5lem3b 592  u2lemaa 601  u3lemaa 602  u4lemaa 603  u5lemaa 604  u3lemana 607  u4lemana 608  u5lemana 609  u3lemab 612  u4lemab 613  u5lemab 614  u1lemanb 615  u3lemanb 617  u4lemanb 618  u5lemanb 619  u2lemle2 716  u4lemle2 718  u5lemle2 719  u5lembi 725  u4lem6 768  u2lem8 782  u3lem13b 790  3vded21 817  mlalem 832  bi3 839  bi4 840  comanblem1 870  marsdenlem3 882  marsdenlem4 883  mlaconjo 886  mhcor1 888  oa3-2lema 978  oa3-1lem 982  oa3-2to2s 990

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