Theorem anor3 90

Description: Conjunction expressed with disjunction. (Contributed by NM, 15-Dec-1997.)

Assertion

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

Proof of Theorem anor3

Step	Hyp	Ref	Expression
1		oran 87	. . 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 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:  mccune2  247  wql2lem2  289  wql2lem5  292  wql1  293  nom40  325  nom41  326  nom42  327  nom43  328  nom44  329  nom45  330  nom50  331  nom51  332  nom52  333  nom53  334  nom54  335  nom55  336  k1-6  353  k1-7  354  k1-4  359  2vwomlem  365  wr5-2v  366  wdf-c2  384  woml6  436  df2c1  468  gstho  491  u1lemnana  645  u2lemnana  646  u3lemnana  647  u4lemnana  648  u5lemnana  649  u2lemnanb  656  u5lemnanb  659  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnob  670  u2lemnob  671  u3lemnob  672  u4lemnob  673  u5lemnob  674  comi12  707  u3lem1n  741  u4lem1n  742  u5lem1n  743  u3lem3n  754  u4lem5n  766  u4lem6  768  u2lem7n  775  u3lem10  785  u3lem11  786  u3lem11a  787  u3lem13a  789  u3lem13b  790  bi1o1a  798  biao  799  i2i1i1  800  3vth1  804  3vth5  808  3vth7  810  3vth9  812  3vded21  817  1oa  820  2oalem1  825  2oath1  826  oale  829  3vroa  831  mlaconj4  844  negantlem7  855  neg3antlem2  865  comanblem1  870  mhlem2  878  mh  879  cancellem  891  e2ast2  894  gomaex3lem1  914  gomaex3lem2  915  gomaex3lem8  921  oa4v3v  934  oa3to4lem6  950  oa6todual  952  oa6fromdual  953  oa8todual  971  oal2  999  oalem1  1005  mloa  1018  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  mldual  1124