Theorem anor2 89

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

Assertion

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

Proof of Theorem anor2

Step	Hyp	Ref	Expression
1		df-a 40	. 2 (a⊥ ∩ b) = (a⊥ ⊥ ∪ b⊥ )⊥
2		ax-a1 30	. . . . 5 a = a⊥ ⊥
3	2	ax-r1 35	. . . 4 a⊥ ⊥ = a
4	3	ax-r5 38	. . 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-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  oran1  91  dff  101  omlem2  128  wwcomd  214  lei3  246  mccune2  247  ni31  250  ud4lem0c  280  ud5lem0c  281  2vwomlem  365  wfh3  425  wfh4  426  fh3  471  fh4  472  i3bi  496  ni32  502  i3th1  543  i3con  551  ud2lem2  564  ud3lem1d  569  ud3lem2  571  ud3lem3  576  ud4lem1a  577  ud4lem1c  579  ud4lem2  582  ud5lem2  590  ud5lem3b  592  ud5lem3c  593  ud5lem3  594  u1lemnaa  640  u2lemnaa  641  u3lemnaa  642  u4lemnaa  643  u5lemnaa  644  u3lemnana  647  u5lemnana  649  u4lemnab  653  u5lemnab  654  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnonb  675  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u3lem1n  741  u4lem1n  742  u5lem1n  743  u3lem3n  754  u1lem11  780  u3lem13a  789  u3lem13b  790  test  802  3vded11  814  neg3antlem2  865  elimcons  868