Theorem oran2 92

Description: Disjunction expressed with conjunction.

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 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

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