Theorem anor1 88

Description: Conjunction expressed with disjunction. (Contributed by NM, 12-Aug-1997.)

Assertion

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

Proof of Theorem anor1

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a ∩ b⊥ ) = (a⊥ ∪ b⊥ ⊥ )⊥
2		ax-a1 30	. . . . 5 b = b⊥ ⊥
3	2	ax-r1 35	. . . 4 b⊥ ⊥ = b
4	3	lor 70	. . 3 (a⊥ ∪ b⊥ ⊥ ) = (a⊥ ∪ b)
5	4	ax-r4 37	. 2 (a⊥ ∪ b⊥ ⊥ )⊥ = (a⊥ ∪ b)⊥
6	1, 5	ax-r2 36	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:  oran2  92  ka4lemo  228  ni31  250  ud4lem0c  280  wcomlem  382  wcom3i  422  comcom  453  com3i  467  i3bi  496  ni32  502  i3th1  543  i3con  551  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1  570  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1d  580  ud4lem1  581  ud5lem1  589  u4lemaa  603  u3lemanb  617  u4lemoa  623  u3lemonb  637  u2lemnaa  641  u3lemnaa  642  u4lemnaa  643  u5lemnaa  644  u1lemnoa  660  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u3lemnona  667  u1lemnob  670  u2lemnob  671  u3lemnob  672  u4lemnob  673  u5lemnob  674  u4lemle2  718  u4lem1n  742  u4lem3n  755  u5lem3n  756  u2lem7n  775  u1lem9a  777  u2lem8  782  u3lemax4  796  3vded22  818  salem1  837  orbi  842  neg3antlem2  865  cancellem  891  gomaex3h10  911  gomaex3lem3  916  oa4v3v  934  wdwom  1106