Theorem oran2 92

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

Assertion

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

Proof of Theorem oran2

Step	Hyp	Ref	Expression
1		anor1 88	. . 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-a2 31  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:  wql2lem3  290  k1-6  353  k1-7  354  wdf-c2  384  u1lemnanb  655  u2lemnanb  656  u3lemnanb  657  u4lemnanb  658  u5lemnanb  659  u3lemnona  667  u4lemnob  673  u4lem5  764  u4lem5n  766  u2lem7n  775  bi4  840  negantlem8  856  neg3antlem2  865  mhlem2  878  marsdenlem3  882  marsdenlem4  883  oa4cl  1027