Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > oran3 | GIF version |
Description: Disjunction expressed with conjunction. (Contributed by NM, 15-Dec-1997.) |
Ref | Expression |
---|---|
oran3 | (a⊥ ∪ b⊥ ) = (a ∩ b)⊥ |
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)⊥ |
Colors of variables: term |
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 |
Copyright terms: Public domain | W3C validator |