Theorem dff 101

Description: Alternate defintion of "false".

Assertion

Ref	Expression
dff	0 = (a ^ a')

Proof of Theorem dff

Step	Hyp	Ref	Expression
1		dff2 100	. 2 0 = (a v a')'
2		ancom 74	. . . 4 (a ^ a') = (a' ^ a)
3		anor2 89	. . . 4 (a' ^ a) = (a v a')'
4	2, 3	ax-r2 36	. . 3 (a ^ a') = (a v a')'
5	4	ax-r1 35	. 2 (a v a')' = (a ^ a')
6	1, 5	ax-r2 36	1 0 = (a ^ a')

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

This theorem is referenced by:  wwfh1 216  wwfh2 217  ska8 236  i3id 251  go1 343  k1-4 359  wfh1 423  wfh2 424  ortha 438  fh1 469  fh2 470  oml4 487  gsth 489  i3bi 496  lem4 511  i3abs3 524  ud2lem1 563  ud3lem1a 566  ud3lem1b 567  ud3lem1d 569  ud3lem2 571  ud3lem3b 573  ud3lem3d 575  ud4lem1a 577  ud4lem1b 578  ud4lem1d 580  ud4lem2 582  ud4lem3 585  ud5lem1a 586  ud5lem1b 587  ud5lem2 590  ud5lem3a 591  ud5lem3b 592  u1lemaa 600  u2lemaa 601  u3lemaa 602  u4lemaa 603  u5lemaa 604  u3lemana 607  u4lemana 608  u5lemana 609  u3lemab 612  u4lemab 613  u5lemab 614  u1lemanb 615  u2lemanb 616  u3lemanb 617  u4lemanb 618  u5lemanb 619  u3lemc4 703  u4lemc4 704  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  u5lembi 725  u2lem1 735  u4lem4 759  u4lem5 764  u4lem6 768  u2lem8 782  u3lem11 786  u3lem13a 789  u3lem13b 790  u3lem15 795  bi1o1a 798  3vded21 817  3vded3 819  1oa 820  mlalem 832  bi3 839  bi4 840  mlaconj4 844  neg3antlem2 865  comanblem1 870  comanblem2 871  mhlem1 877  mh 879  marsdenlem2 881  marsdenlem3 882  marsdenlem4 883  mlaconjo 886  mhcor1 888  govar 896  oa3-6to3 987  oa3-2to4 988  lem3.3.7i3e1 1065

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  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