Theorem oran3 85

Description: Disjunction expressed with conjunction.

Assertion

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

Proof of Theorem oran3

Step	Hyp	Ref	Expression
1		df-a 39	. . 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  wql2lem5 284  oaidlem1 286  womle2a 287  nom15 304  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  nom25 310  go1 335  2vwomlem 347  wdf-c2 366  ska2 414  ska4 415  u3lemnana 629  u5lemnana 631  u4lemnab 635  u5lemnab 636  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u1lemnonb 657  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u3lem3n 736  u4lem3n 737  u5lem3n 738  u4lem5 746  u2lem7n 757  u3lem13a 771  u3lem13b 772  u3lemax4 778  u3lemax5 779  test 784  3vcom 795  1oai1 803  2oath1i1 809  mlalem 814  sadm3 820  elimconslem 849  mh 861  mlaconjolem 867  mlaconjo 868  oaidlem2 911  oaidlem2g 912  oa4v3v 914  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa8todual 951

This theorem was proved from axioms:  ax-a1 29  ax-r1 34  ax-r2 35  ax-r4 36

This theorem depends on definitions:  df-a 39

metamath.org