Theorem oran3 93

Description: Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.)

Assertion

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

Proof of Theorem oran3

Step	Hyp	Ref	Expression
1		df-a 40	. . 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-r1 35  ax-r2 36  ax-r4 37

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  mccune2  247  wql2lem5  292  oaidlem1  294  womle2a  295  nom15  312  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  nom25  318  go1  343  k1-6  353  k1-7  354  2vwomlem  365  wdf-c2  384  ska2  432  ska4  433  u3lemnana  647  u5lemnana  649  u4lemnab  653  u5lemnab  654  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u1lemnonb  675  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u3lem3n  754  u4lem3n  755  u5lem3n  756  u4lem5  764  u2lem7n  775  u3lem13a  789  u3lem13b  790  u3lemax4  796  u3lemax5  797  test  802  3vcom  813  1oai1  821  2oath1i1  827  mlalem  832  sadm3  838  elimconslem  867  mh  879  mlaconjolem  885  mlaconjo  886  oaidlem2  931  oaidlem2g  932  oa4v3v  934  oa3to4lem6  950  oa6todual  952  oa6fromdual  953  oa8todual  971  lem3.3.4  1053  lem3.3.7i0e1  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e2  1067  mldual  1124