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) v a) = 1
Theorem	u2lemoa 603	Lemma for Dishkant implication study.
((a ->2 b) v a) = 1
Theorem	u3lemoa 604	Lemma for Kalmbach implication study.
((a ->3 b) v a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u4lemoa 605	Lemma for non-tollens implication study.
((a ->4 b) v a) = 1
Theorem	u5lemoa 606	Lemma for relevance implication study.
((a ->5 b) v a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u1lemona 607	Lemma for Sasaki implication study.
((a ->1 b) v a_|_) = (a_|_ v (a ^ b))
Theorem	u2lemona 608	Lemma for Dishkant implication study.
((a ->2 b) v a_|_) = (a_|_ v b)
Theorem	u3lemona 609	Lemma for Kalmbach implication study.
((a ->3 b) v a_|_) = (a_|_ v b)
Theorem	u4lemona 610	Lemma for non-tollens implication study.
((a ->4 b) v a_|_) = (a_|_ v b)
Theorem	u5lemona 611	Lemma for relevance implication study.
((a ->5 b) v a_|_) = (a_|_ v (a ^ b))
Theorem	u1lemob 612	Lemma for Sasaki implication study.
((a ->1 b) v b) = (a_|_ v b)
Theorem	u2lemob 613	Lemma for Dishkant implication study.
((a ->2 b) v b) = ((a_|_ ^ b_|_) v b)
Theorem	u3lemob 614	Lemma for Kalmbach implication study.
((a ->3 b) v b) = (a_|_ v b)
Theorem	u4lemob 615	Lemma for non-tollens implication study.
((a ->4 b) v b) = (a_|_ v b)
Theorem	u5lemob 616	Lemma for relevance implication study.
((a ->5 b) v b) = ((a_|_ ^ b_|_) v b)
Theorem	u1lemonb 617	Lemma for Sasaki implication study.
((a ->1 b) v b_|_) = 1
Theorem	u2lemonb 618	Lemma for Dishkant implication study.
((a ->2 b) v b_|_) = 1
Theorem	u3lemonb 619	Lemma for Kalmbach implication study.
((a ->3 b) v b_|_) = 1
Theorem	u4lemonb 620	Lemma for non-tollens implication study.
((a ->4 b) v b_|_) = (((a ^ b) v (a_|_ ^ b)) v b_|_)
Theorem	u5lemonb 621	Lemma for relevance implication study.
((a ->5 b) v b_|_) = (((a ^ b) v (a_|_ ^ b)) v b_|_)
Theorem	u1lemnaa 622	Lemma for Sasaki implication study.
((a ->1 b)_|_ ^ a) = (a ^ (a_|_ v 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_|_ v 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 v b) ^ (a v 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 v b) ^ (a v 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 v b_|_) ^ (a_|_ v b_|_)) ^ b)
Theorem	u5lemnab 636	Lemma for relevance implication study.
((a ->5 b)_|_ ^ b) = (((a v b_|_) ^ (a_|_ v 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 v 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 v b) ^ b_|_)
Theorem	u1lemnoa 642	Lemma for Sasaki implication study.
((a ->1 b)_|_ v a) = a
Theorem	u2lemnoa 643	Lemma for Dishkant implication study.
((a ->2 b)_|_ v a) = ((a v b) ^ (a v b_|_))
Theorem	u3lemnoa 644	Lemma for Kalmbach implication study.
((a ->3 b)_|_ v a) = ((a v b) ^ (a v b_|_))
Theorem	u4lemnoa 645	Lemma for non-tollens implication study.
((a ->4 b)_|_ v a) = ((a v b) ^ (a v b_|_))
Theorem	u5lemnoa 646	Lemma for relevance implication study.
((a ->5 b)_|_ v a) = ((a v b) ^ (a v b_|_))
Theorem	u1lemnona 647	Lemma for Sasaki implication study.
((a ->1 b)_|_ v a_|_) = (a_|_ v b_|_)
Theorem	u2lemnona 648	Lemma for Dishkant implication study.
((a ->2 b)_|_ v a_|_) = (a_|_ v b_|_)
Theorem	u3lemnona 649	Lemma for Kalmbach implication study.
((a ->3 b)_|_ v a_|_) = (a_|_ v (a ^ b_|_))
Theorem	u4lemnona 650	Lemma for non-tollens implication study.
((a ->4 b)_|_ v a_|_) = (a_|_ v b_|_)
Theorem	u5lemnona 651	Lemma for relevance implication study.
((a ->5 b)_|_ v a_|_) = (a_|_ v b_|_)
Theorem	u1lemnob 652	Lemma for Sasaki implication study.
((a ->1 b)_|_ v b) = (a v b)
Theorem	u2lemnob 653	Lemma for Dishkant implication study.
((a ->2 b)_|_ v b) = (a v b)
Theorem	u3lemnob 654	Lemma for Kalmbach implication study.
((a ->3 b)_|_ v b) = (a v b)
Theorem	u4lemnob 655	Lemma for non-tollens implication study.
((a ->4 b)_|_ v b) = ((a ^ b_|_) v b)
Theorem	u5lemnob 656	Lemma for relevance implication study.
((a ->5 b)_|_ v b) = (a v b)
Theorem	u1lemnonb 657	Lemma for Sasaki implication study.
((a ->1 b)_|_ v b_|_) = ((a v b_|_) ^ (a_|_ v b_|_))
Theorem	u2lemnonb 658	Lemma for Dishkant implication study.
((a ->2 b)_|_ v b_|_) = b_|_
Theorem	u3lemnonb 659	Lemma for Kalmbach implication study.
((a ->3 b)_|_ v b_|_) = ((a v b_|_) ^ (a_|_ v b_|_))
Theorem	u4lemnonb 660	Lemma for non-tollens implication study.
((a ->4 b)_|_ v b_|_) = ((a v b_|_) ^ (a_|_ v b_|_))
Theorem	u5lemnonb 661	Lemma for relevance implication study.
((a ->5 b)_|_ v b_|_) = ((a v b_|_) ^ (a_|_ v 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_|_ v b)
Theorem	u2lemc4 684	Lemma for Dishkant implication study.
a C b   =>   (a ->2 b) = (a_|_ v b)
Theorem	u3lemc4 685	Lemma for Kalmbach implication study.
a C b   =>   (a ->3 b) = (a_|_ v b)
Theorem	u4lemc4 686	Lemma for non-tollens implication study.
a C b   =>   (a ->4 b) = (a_|_ v b)
Theorem	u5lemc4 687	Lemma for relevance implication study.
a C b   =>   (a ->5 b) = (a_|_ v 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