Theorem oran3 93

Description: Disjunction expressed with conjunction.

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 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 1052  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e2 1066

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

Copyright terms: Public domain