Theorem anor3 90

Description: Conjunction expressed with disjunction.

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 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  ska2 432  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 1052  lem3.3.6 1055  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066

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

Copyright terms: Public domain