Theorem anor2 81

Description: Conjunction expressed with disjunction.

Assertion

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

Proof of Theorem anor2

Step	Hyp	Ref	Expression
1		df-a 39	. 2 (a⊥ ∩ b) = (a⊥ ⊥ ∪ b⊥ )⊥
2		ax-a1 29	. . . . 5 a = a⊥ ⊥
3	2	ax-r1 34	. . . 4 a⊥ ⊥ = a
4	3	ax-r5 37	. . 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:  oran1 83  dff 93  omlem2 120  wwcomd 206  lei3 238  mccune2 239  ni31 242  ud4lem0c 272  ud5lem0c 273  2vwomlem 347  wfh3 407  wfh4 408  fh3 453  fh4 454  i3bi 478  ni32 484  i3th1 525  i3con 533  ud2lem2 546  ud3lem1d 551  ud3lem2 553  ud3lem3 558  ud4lem1a 559  ud4lem1c 561  ud4lem2 564  ud5lem2 572  ud5lem3b 574  ud5lem3c 575  ud5lem3 576  u1lemnaa 622  u2lemnaa 623  u3lemnaa 624  u4lemnaa 625  u5lemnaa 626  u3lemnana 629  u5lemnana 631  u4lemnab 635  u5lemnab 636  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u3lem1n 723  u4lem1n 724  u5lem1n 725  u3lem3n 736  u1lem11 762  u3lem13a 771  u3lem13b 772  test 784  3vded11 796  neg3antlem2 847  elimcons 850

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

This theorem depends on definitions:  df-a 39

metamath.org