Theorem anor3 82

Description: Conjunction expressed with disjunction.

Assertion

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

Proof of Theorem anor3

Step	Hyp	Ref	Expression
1		oran 79	. . 3 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
2	1	ax-r1 34	. 2 (a⊥ ∩ b⊥ )⊥ = (a ∪ b)
3	2	con3 65	1 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥

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

This theorem is referenced by:  mccune2 239  wql2lem2 281  wql2lem5 284  wql1 285  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  2vwomlem 347  wr5-2v 348  wdf-c2 366  ska2 414  woml6 418  df2c1 450  gstho 473  u1lemnana 627  u2lemnana 628  u3lemnana 629  u4lemnana 630  u5lemnana 631  u2lemnanb 638  u5lemnanb 641  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnob 652  u2lemnob 653  u3lemnob 654  u4lemnob 655  u5lemnob 656  comi12 689  u3lem1n 723  u4lem1n 724  u5lem1n 725  u3lem3n 736  u4lem5n 748  u4lem6 750  u2lem7n 757  u3lem10 767  u3lem11 768  u3lem11a 769  u3lem13a 771  u3lem13b 772  bi1o1a 780  biao 781  i2i1i1 782  3vth1 786  3vth5 790  3vth7 792  3vth9 794  3vded21 799  1oa 802  2oalem1 807  2oath1 808  oale 811  3vroa 813  mlaconj4 826  negantlem7 837  neg3antlem2 847  comanblem1 852  mhlem2 860  mh 861  cancellem 873  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem8 901  oa4v3v 914  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa8todual 951  oal2 979  oalem1 985  mloa 998

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