Theorem anor1 80

Description: Conjunction expressed with disjunction.

Assertion

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

Proof of Theorem anor1

Step	Hyp	Ref	Expression
1		df-a 39	. 2 (a ∩ b⊥ ) = (a⊥ ∪ b⊥ ⊥ )⊥
2		ax-a1 29	. . . . 5 b = b⊥ ⊥
3	2	ax-r1 34	. . . 4 b⊥ ⊥ = b
4	3	lor 66	. . 3 (a⊥ ∪ b⊥ ⊥ ) = (a⊥ ∪ b)
5	4	ax-r4 36	. 2 (a⊥ ∪ b⊥ ⊥ )⊥ = (a⊥ ∪ b)⊥
6	1, 5	ax-r2 35	1 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥

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

This theorem is referenced by:  oran2 84  ka4lemo 220  ni31 242  ud4lem0c 272  wcomlem 364  wcom3i 404  comcom 435  com3i 449  i3bi 478  ni32 484  i3th1 525  i3con 533  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1 552  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1d 562  ud4lem1 563  ud5lem1 571  u4lemaa 585  u3lemanb 599  u4lemoa 605  u3lemonb 619  u2lemnaa 623  u3lemnaa 624  u4lemnaa 625  u5lemnaa 626  u1lemnoa 642  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u3lemnona 649  u1lemnob 652  u2lemnob 653  u3lemnob 654  u4lemnob 655  u5lemnob 656  u4lemle2 700  u4lem1n 724  u4lem3n 737  u5lem3n 738  u2lem7n 757  u1lem9a 759  u2lem8 764  u3lemax4 778  3vded22 800  salem1 819  orbi 824  neg3antlem2 847  cancellem 873  gomaex3h10 891  gomaex3lem3 896  oa4v3v 914

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39

metamath.org