Theorem oran1 91

Description: Disjunction expressed with conjunction.

Assertion

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

Proof of Theorem oran1

Step	Hyp	Ref	Expression
1		anor2 89	. . 3 (a' ^ b) = (a v b')'
2	1	ax-r1 35	. 2 (a v b')' = (a' ^ b)
3	2	con3 68	1 (a v b') = (a' ^ b)'

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

This theorem is referenced by:  k1-4 359  u3lemnana 647  u5lemnana 649  u1lemnab 650  u2lemnab 651  u3lemnab 652  u4lemnab 653  u5lemnab 654  u4lem1n 742  u3lem3n 754  u4lem5 764  u3lem10 785  u3lem11 786  u3lem11a 787  neg3antlem2 865  marsdenlem4 883  mlaconjo 886  oa4v3v 934  lem3.3.4 1052

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