Quantum Logic Explorer - mmtheorems7

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1024

Statement List for Quantum Logic Explorer - 601-700 - Page 7 of 11

Type	Label	Description
Statement
Theorem	u5lemanb 601	Lemma for relevance implication study.
((a →5 b) ∩ b⊥ ) = (a⊥ ∩ b⊥ )
Theorem	u1lemoa 602	Lemma for Sasaki implication study.
((a →1 b) ∪ a) = 1
Theorem	u2lemoa 603	Lemma for Dishkant implication study.
((a →2 b) ∪ a) = 1
Theorem	u3lemoa 604	Lemma for Kalmbach implication study.
((a →3 b) ∪ a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lemoa 605	Lemma for non-tollens implication study.
((a →4 b) ∪ a) = 1
Theorem	u5lemoa 606	Lemma for relevance implication study.
((a →5 b) ∪ a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u1lemona 607	Lemma for Sasaki implication study.
((a →1 b) ∪ a⊥ ) = (a⊥ ∪ (a ∩ b))
Theorem	u2lemona 608	Lemma for Dishkant implication study.
((a →2 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u3lemona 609	Lemma for Kalmbach implication study.
((a →3 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u4lemona 610	Lemma for non-tollens implication study.
((a →4 b) ∪ a⊥ ) = (a⊥ ∪ b)
Theorem	u5lemona 611	Lemma for relevance implication study.
((a →5 b) ∪ a⊥ ) = (a⊥ ∪ (a ∩ b))
Theorem	u1lemob 612	Lemma for Sasaki implication study.
((a →1 b) ∪ b) = (a⊥ ∪ b)
Theorem	u2lemob 613	Lemma for Dishkant implication study.
((a →2 b) ∪ b) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u3lemob 614	Lemma for Kalmbach implication study.
((a →3 b) ∪ b) = (a⊥ ∪ b)
Theorem	u4lemob 615	Lemma for non-tollens implication study.
((a →4 b) ∪ b) = (a⊥ ∪ b)
Theorem	u5lemob 616	Lemma for relevance implication study.
((a →5 b) ∪ b) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u1lemonb 617	Lemma for Sasaki implication study.
((a →1 b) ∪ b⊥ ) = 1
Theorem	u2lemonb 618	Lemma for Dishkant implication study.
((a →2 b) ∪ b⊥ ) = 1
Theorem	u3lemonb 619	Lemma for Kalmbach implication study.
((a →3 b) ∪ b⊥ ) = 1
Theorem	u4lemonb 620	Lemma for non-tollens implication study.
((a →4 b) ∪ b⊥ ) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b⊥ )
Theorem	u5lemonb 621	Lemma for relevance implication study.
((a →5 b) ∪ b⊥ ) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ b⊥ )
Theorem	u1lemnaa 622	Lemma for Sasaki implication study.
((a →1 b)⊥ ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	u2lemnaa 623	Lemma for Dishkant implication study.
((a →2 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u3lemnaa 624	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u4lemnaa 625	Lemma for non-tollens implication study.
((a →4 b)⊥ ∩ a) = (a ∩ b⊥ )
Theorem	u5lemnaa 626	Lemma for relevance implication study.
((a →5 b)⊥ ∩ a) = (a ∩ (a⊥ ∪ b⊥ ))
Theorem	u1lemnana 627	Lemma for Sasaki implication study.
((a →1 b)⊥ ∩ a⊥ ) = 0
Theorem	u2lemnana 628	Lemma for Dishkant implication study.
((a →2 b)⊥ ∩ a⊥ ) = 0
Theorem	u3lemnana 629	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u4lemnana 630	Lemma for non-tollens implication study.
((a →4 b)⊥ ∩ a⊥ ) = 0
Theorem	u5lemnana 631	Lemma for relevance implication study.
((a →5 b)⊥ ∩ a⊥ ) = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u1lemnab 632	Lemma for Sasaki implication study.
((a →1 b)⊥ ∩ b) = 0
Theorem	u2lemnab 633	Lemma for Dishkant implication study.
((a →2 b)⊥ ∩ b) = 0
Theorem	u3lemnab 634	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∩ b) = 0
Theorem	u4lemnab 635	Lemma for non-tollens implication study.
((a →4 b)⊥ ∩ b) = (((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ )) ∩ b)
Theorem	u5lemnab 636	Lemma for relevance implication study.
((a →5 b)⊥ ∩ b) = (((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ )) ∩ b)
Theorem	u1lemnanb 637	Lemma for Sasaki implication study.
((a →1 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u2lemnanb 638	Lemma for Dishkant implication study.
((a →2 b)⊥ ∩ b⊥ ) = ((a ∪ b) ∩ b⊥ )
Theorem	u3lemnanb 639	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u4lemnanb 640	Lemma for non-tollens implication study.
((a →4 b)⊥ ∩ b⊥ ) = (a ∩ b⊥ )
Theorem	u5lemnanb 641	Lemma for relevance implication study.
((a →5 b)⊥ ∩ b⊥ ) = ((a ∪ b) ∩ b⊥ )
Theorem	u1lemnoa 642	Lemma for Sasaki implication study.
((a →1 b)⊥ ∪ a) = a
Theorem	u2lemnoa 643	Lemma for Dishkant implication study.
((a →2 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u3lemnoa 644	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u4lemnoa 645	Lemma for non-tollens implication study.
((a →4 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u5lemnoa 646	Lemma for relevance implication study.
((a →5 b)⊥ ∪ a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u1lemnona 647	Lemma for Sasaki implication study.
((a →1 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u2lemnona 648	Lemma for Dishkant implication study.
((a →2 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u3lemnona 649	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∪ a⊥ ) = (a⊥ ∪ (a ∩ b⊥ ))
Theorem	u4lemnona 650	Lemma for non-tollens implication study.
((a →4 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u5lemnona 651	Lemma for relevance implication study.
((a →5 b)⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
Theorem	u1lemnob 652	Lemma for Sasaki implication study.
((a →1 b)⊥ ∪ b) = (a ∪ b)
Theorem	u2lemnob 653	Lemma for Dishkant implication study.
((a →2 b)⊥ ∪ b) = (a ∪ b)
Theorem	u3lemnob 654	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∪ b) = (a ∪ b)
Theorem	u4lemnob 655	Lemma for non-tollens implication study.
((a →4 b)⊥ ∪ b) = ((a ∩ b⊥ ) ∪ b)
Theorem	u5lemnob 656	Lemma for relevance implication study.
((a →5 b)⊥ ∪ b) = (a ∪ b)
Theorem	u1lemnonb 657	Lemma for Sasaki implication study.
((a →1 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u2lemnonb 658	Lemma for Dishkant implication study.
((a →2 b)⊥ ∪ b⊥ ) = b⊥
Theorem	u3lemnonb 659	Lemma for Kalmbach implication study.
((a →3 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u4lemnonb 660	Lemma for non-tollens implication study.
((a →4 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u5lemnonb 661	Lemma for relevance implication study.
((a →5 b)⊥ ∪ b⊥ ) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ b⊥ ))
Theorem	u1lemc1 662	Commutation theorem for Sasaki implication.
a C (a →1 b)
Theorem	u2lemc1 663	Commutation theorem for Dishkant implication.
b C (a →2 b)
Theorem	u3lemc1 664	Commutation theorem for Kalmbach implication.
a C (a →3 b)
Theorem	u4lemc1 665	Commutation theorem for non-tollens implication.
b C (a →4 b)
Theorem	u5lemc1 666	Commutation theorem for relevance implication.
a C (a →5 b)
Theorem	u5lemc1b 667	Commutation theorem for relevance implication.
b C (a →5 b)
Theorem	u1lemc2 668	Commutation theorem for Sasaki implication.
a C b    &   a C c    ⇒   a C (b →1 c)
Theorem	u2lemc2 669	Commutation theorem for Dishkant implication.
a C b    &   a C c    ⇒   a C (b →2 c)
Theorem	u3lemc2 670	Commutation theorem for Kalmbach implication.
a C b    &   a C c    ⇒   a C (b →3 c)
Theorem	u4lemc2 671	Commutation theorem for non-tollens implication.
a C b    &   a C c    ⇒   a C (b →4 c)
Theorem	u5lemc2 672	Commutation theorem for relevance implication.
a C b    &   a C c    ⇒   a C (b →5 c)
Theorem	u1lemc3 673	Commutation theorem for Sasaki implication.
a C b    ⇒   a C (b →1 a)
Theorem	u2lemc3 674	Commutation theorem for Dishkant implication.
a C b    ⇒   a C (b →2 a)
Theorem	u3lemc3 675	Commutation theorem for Kalmbach implication.
a C b    ⇒   a C (b →3 a)
Theorem	u4lemc3 676	Commutation theorem for non-tollens implication.
a C b    ⇒   a C (b →4 a)
Theorem	u5lemc3 677	Commutation theorem for relevance implication.
a C b    ⇒   a C (b →5 a)
Theorem	u1lemc5 678	Commutation theorem for Sasaki implication.
a C b    ⇒   a C (a →1 b)
Theorem	u2lemc5 679	Commutation theorem for Dishkant implication.
a C b    ⇒   a C (a →2 b)
Theorem	u3lemc5 680	Commutation theorem for Kalmbach implication.
a C b    ⇒   a C (a →3 b)
Theorem	u4lemc5 681	Commutation theorem for non-tollens implication.
a C b    ⇒   a C (a →4 b)
Theorem	u5lemc5 682	Commutation theorem for relevance implication.
a C b    ⇒   a C (a →5 b)
Theorem	u1lemc4 683	Lemma for Sasaki implication study.
a C b    ⇒   (a →1 b) = (a⊥ ∪ b)
Theorem	u2lemc4 684	Lemma for Dishkant implication study.
a C b    ⇒   (a →2 b) = (a⊥ ∪ b)
Theorem	u3lemc4 685	Lemma for Kalmbach implication study.
a C b    ⇒   (a →3 b) = (a⊥ ∪ b)
Theorem	u4lemc4 686	Lemma for non-tollens implication study.
a C b    ⇒   (a →4 b) = (a⊥ ∪ b)
Theorem	u5lemc4 687	Lemma for relevance implication study.
a C b    ⇒   (a →5 b) = (a⊥ ∪ b)
Theorem	u1lemc6 688	Commutation theorem for Sasaki implication.
(a →1 b) C (a⊥ →1 b)
Theorem	comi12 689	Commutation theorem for →1 and →2 .
(a →1 b) C (c →2 a)
Theorem	i1com 690	Commutation expressed with →1 .
b ≤ (a →1 b)    ⇒   a C b
Theorem	comi1 691	Commutation expressed with →1 .
a C b    ⇒   b ≤ (a →1 b)
Theorem	u1lemle1 692	L.e. to Sasaki implication.
a ≤ b    ⇒   (a →1 b) = 1
Theorem	u2lemle1 693	L.e. to Dishkant implication.
a ≤ b    ⇒   (a →2 b) = 1
Theorem	u3lemle1 694	L.e. to Kalmbach implication.
a ≤ b    ⇒   (a →3 b) = 1
Theorem	u4lemle1 695	L.e. to non-tollens implication.
a ≤ b    ⇒   (a →4 b) = 1
Theorem	u5lemle1 696	L.e. to relevance implication.
a ≤ b    ⇒   (a →5 b) = 1
Theorem	u1lemle2 697	Sasaki implication to l.e.
(a →1 b) = 1    ⇒   a ≤ b
Theorem	u2lemle2 698	Dishkant implication to l.e.
(a →2 b) = 1    ⇒   a ≤ b
Theorem	u3lemle2 699	Kalmbach implication to l.e.
(a →3 b) = 1    ⇒   a ≤ b
Theorem	u4lemle2 700	Non-tollens implication to l.e.
(a →4 b) = 1    ⇒   a ≤ b