Theorem oran1 91

Description: Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)

Assertion

Ref	Expression
oran1	(a ∪ b⊥ ) = (a⊥ ∩ b)⊥

Proof of Theorem oran1

Step	Hyp	Ref	Expression
1		anor2 89	. . 3 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
2	1	ax-r1 35	. 2 (a ∪ b⊥ )⊥ = (a⊥ ∩ b)
3	2	con3 68	1 (a ∪ b⊥ ) = (a⊥ ∩ b)⊥

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

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  1053