Theorem anor1 88

Description: Conjunction expressed with disjunction.

Assertion

Ref	Expression
anor1	(a ^ b') = (a' v b)'

Proof of Theorem anor1

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ^ b') = (a' v b'')'
2		ax-a1 30	. . . . 5 b = b''
3	2	ax-r1 35	. . . 4 b'' = b
4	3	lor 70	. . 3 (a' v b'') = (a' v b)
5	4	ax-r4 37	. 2 (a' v b'')' = (a' v b)'
6	1, 5	ax-r2 36	1 (a ^ b') = (a' v b)'

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

This theorem is referenced by:  oran2 92  ka4lemo 228  ni31 250  ud4lem0c 280  wcomlem 382  wcom3i 422  comcom 453  com3i 467  i3bi 496  ni32 502  i3th1 543  i3con 551  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1 570  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1d 580  ud4lem1 581  ud5lem1 589  u4lemaa 603  u3lemanb 617  u4lemoa 623  u3lemonb 637  u2lemnaa 641  u3lemnaa 642  u4lemnaa 643  u5lemnaa 644  u1lemnoa 660  u2lemnoa 661  u3lemnoa 662  u4lemnoa 663  u5lemnoa 664  u3lemnona 667  u1lemnob 670  u2lemnob 671  u3lemnob 672  u4lemnob 673  u5lemnob 674  u4lemle2 718  u4lem1n 742  u4lem3n 755  u5lem3n 756  u2lem7n 775  u1lem9a 777  u2lem8 782  u3lemax4 796  3vded22 818  salem1 837  orbi 842  neg3antlem2 865  cancellem 891  gomaex3h10 911  gomaex3lem3 916  oa4v3v 934  wdwom 1103

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

Copyright terms: Public domain