Theorem anor2 89

Description: Conjunction expressed with disjunction.

Assertion

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

Proof of Theorem anor2

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a' ^ b) = (a'' v b')'
2		ax-a1 30	. . . . 5 a = a''
3	2	ax-r1 35	. . . 4 a'' = a
4	3	ax-r5 38	. . 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:  oran1 91  dff 101  omlem2 128  wwcomd 214  lei3 246  mccune2 247  ni31 250  ud4lem0c 280  ud5lem0c 281  2vwomlem 365  wfh3 425  wfh4 426  fh3 471  fh4 472  i3bi 496  ni32 502  i3th1 543  i3con 551  ud2lem2 564  ud3lem1d 569  ud3lem2 571  ud3lem3 576  ud4lem1a 577  ud4lem1c 579  ud4lem2 582  ud5lem2 590  ud5lem3b 592  ud5lem3c 593  ud5lem3 594  u1lemnaa 640  u2lemnaa 641  u3lemnaa 642  u4lemnaa 643  u5lemnaa 644  u3lemnana 647  u5lemnana 649  u4lemnab 653  u5lemnab 654  u2lemnoa 661  u3lemnoa 662  u4lemnoa 663  u5lemnoa 664  u1lemnonb 675  u3lemnonb 677  u4lemnonb 678  u5lemnonb 679  u3lem1n 741  u4lem1n 742  u5lem1n 743  u3lem3n 754  u1lem11 780  u3lem13a 789  u3lem13b 790  test 802  3vded11 814  neg3antlem2 865  elimcons 868

This theorem was proved from axioms:  ax-a1 30  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40

Copyright terms: Public domain