Quantum Logic Explorer - mmtheorems8

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 - 701-800 - Page 8 of 11

Type	Label	Description
Statement
Theorem	u5lemle2 701	Relevance implication to l.e.
(a ->5 b) = 1   =>   a =< b
Theorem	u1lembi 702	Sasaki implication and biconditional.
((a ->1 b) ^ (b ->1 a)) = (a == b)
Theorem	u2lembi 703	Dishkant implication and biconditional.
((a ->2 b) ^ (b ->2 a)) = (a == b)
Theorem	i2bi 704	Dishkant implication expressed with biconditional.
(a ->2 b) = (b v (a == b))
Theorem	u3lembi 705	Kalmbach implication and biconditional.
((a ->3 b) ^ (b ->3 a)) = (a == b)
Theorem	u4lembi 706	Non-tollens implication and biconditional.
((a ->4 b) ^ (b ->4 a)) = (a == b)
Theorem	u5lembi 707	Relevance implication and biconditional.
((a ->5 b) ^ (b ->5 a)) = (a == b)
Theorem	u12lembi 708	Sasaki/Dishkant implication and biconditional.
((a ->1 b) ^ (b ->2 a)) = (a == b)
Theorem	u21lembi 709	Dishkant/Sasaki implication and biconditional.
((a ->2 b) ^ (b ->1 a)) = (a == b)
Theorem	ublemc1 710	Commutation theorem for biimplication.
a C (a == b)
Theorem	ublemc2 711	Commutation theorem for biimplication.
b C (a == b)
Theorem	u1lemn1b 712	This theorem continues the line of proofs such as u1lemnaa 622, ud1lem0b 248, u1lemnanb 637, etc. (Contributed by Josiah Burroughs 26-May-04.)
(a ->1 b) = ((a ->1 b)_|_ ->1 b)
Theorem	u1lem3var1 713	A 3-variable formula. (Contributed by Josiah Burroughs 26-May-04.)
(((a ->1 c) ^ (b ->1 c))_|_ v (((a ->1 c)_|_ ->1 c) ^ ((b ->1 c)_|_ ->1 c))) = 1
Theorem	oi3oa3lem1 714	An attempt at the OA3 conjecture, which is true if (a == b) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (b == a)   =>   (((a ->1 c) ^ (b ->1 c)) v (a ^ b)) = 1
Theorem	oi3oa3 715	An attempt at the OA3 conjecture, which is true if (a == b) = 1. (Contributed by Josiah Burroughs 27-May-04.)
1 = (b == a)   =>   (((a ->1 c) ^ (b ->1 c)) v ((((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v (a ^ b))) ->1 c) ^ (((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v (a ^ b))) ->1 c))) = 1
Theorem	u1lem1 716	Lemma for unified implication study.
((a ->1 b) ->1 a) = a
Theorem	u2lem1 717	Lemma for unified implication study.
((a ->2 b) ->2 a) = a
Theorem	u3lem1 718	Lemma for unified implication study.
((a ->3 b) ->3 a) = ((a v b) ^ (a v b_|_))
Theorem	u4lem1 719	Lemma for unified implication study.
((a ->4 b) ->4 a) = ((((a ^ b) v (a ^ b_|_)) v a_|_) ^ ((a v b) ^ (a v b_|_)))
Theorem	u5lem1 720	Lemma for unified implication study.
((a ->5 b) ->5 a) = ((a v b) ^ (a v b_|_))
Theorem	u1lem1n 721	Lemma for unified implication study.
((a ->1 b) ->1 a)_|_ = a_|_
Theorem	u2lem1n 722	Lemma for unified implication study.
((a ->2 b) ->2 a)_|_ = a_|_
Theorem	u3lem1n 723	Lemma for unified implication study.
((a ->3 b) ->3 a)_|_ = ((a_|_ ^ b) v (a_|_ ^ b_|_))
Theorem	u4lem1n 724	Lemma for unified implication study.
((a ->4 b) ->4 a)_|_ = ((((a_|_ v b) ^ (a_|_ v b_|_)) ^ a) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u5lem1n 725	Lemma for unified implication study.
((a ->5 b) ->5 a)_|_ = ((a_|_ ^ b) v (a_|_ ^ b_|_))
Theorem	u1lem2 726	Lemma for unified implication study.
(((a ->1 b) ->1 a) ->1 a) = 1
Theorem	u2lem2 727	Lemma for unified implication study.
(((a ->2 b) ->2 a) ->2 a) = 1
Theorem	u3lem2 728	Lemma for unified implication study.
(((a ->3 b) ->3 a) ->3 a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u4lem2 729	Lemma for unified implication study.
(((a ->4 b) ->4 a) ->4 a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u5lem2 730	Lemma for unified implication study.
(((a ->5 b) ->5 a) ->5 a) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u1lem3 731	Lemma for unified implication study.
(a ->1 (b ->1 a)) = (a_|_ v ((a ^ b) v (a ^ b_|_)))
Theorem	u2lem3 732	Lemma for unified implication study.
(a ->2 (b ->2 a)) = 1
Theorem	u3lem3 733	Lemma for unified implication study.
(a ->3 (b ->3 a)) = (a v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
Theorem	u4lem3 734	Lemma for unified implication study.
(a ->4 (b ->4 a)) = (a_|_ v ((a ^ b) v (a ^ b_|_)))
Theorem	u5lem3 735	Lemma for unified implication study.
(a ->5 (b ->5 a)) = (a_|_ v ((a ^ b) v (a ^ b_|_)))
Theorem	u3lem3n 736	Lemma for unified implication study.
(a ->3 (b ->3 a))_|_ = (a_|_ ^ ((a v b) ^ (a v b_|_)))
Theorem	u4lem3n 737	Lemma for unified implication study.
(a ->4 (b ->4 a))_|_ = (a ^ ((a_|_ v b) ^ (a_|_ v b_|_)))
Theorem	u5lem3n 738	Lemma for unified implication study.
(a ->5 (b ->5 a))_|_ = (a ^ ((a_|_ v b) ^ (a_|_ v b_|_)))
Theorem	u1lem4 739	Lemma for unified implication study.
(a ->1 (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))
Theorem	u3lem4 740	Lemma for unified implication study.
(a ->3 (a ->3 (b ->3 a))) = 1
Theorem	u4lem4 741	Lemma for unified implication study.
(a ->4 (a ->4 (b ->4 a))) = (a ->4 (b ->4 a))
Theorem	u5lem4 742	Lemma for unified implication study.
(a ->5 (a ->5 (b ->5 a))) = (a ->5 (b ->5 a))
Theorem	u1lem5 743	Lemma for unified implication study.
(a ->1 (a ->1 b)) = (a ->1 b)
Theorem	u2lem5 744	Lemma for unified implication study.
(a ->2 (a ->2 b)) = (a ->2 b)
Theorem	u3lem5 745	Lemma for unified implication study.
(a ->3 (a ->3 b)) = (a_|_ v b)
Theorem	u4lem5 746	Lemma for unified implication study.
(a ->4 (a ->4 b)) = ((a_|_ ^ b_|_) v b)
Theorem	u5lem5 747	Lemma for unified implication study.
(a ->5 (a ->5 b)) = (a_|_ v (a ^ b))
Theorem	u4lem5n 748	Lemma for unified implication study.
(a ->4 (a ->4 b))_|_ = ((a v b) ^ b_|_)
Theorem	u3lem6 749	Lemma for unified implication study.
(a ->3 (a ->3 (a ->3 b))) = (a ->3 (a ->3 b))
Theorem	u4lem6 750	Lemma for unified implication study.
(a ->4 (a ->4 (a ->4 b))) = (a ->4 b)
Theorem	u5lem6 751	Lemma for unified implication study.
(a ->5 (a ->5 (a ->5 b))) = (a ->5 (a ->5 b))
Theorem	u24lem 752	Lemma for unified implication study.
((a ->2 b) ^ (a ->4 b)) = (a ->5 b)
Theorem	u12lem 753	Implication lemma.
((a ->1 b) v (a ->2 b)) = (a ->0 b)
Theorem	u1lem7 754	Lemma for unified implication study.
(a ->1 (a_|_ ->1 b)) = 1
Theorem	u2lem7 755	Lemma for unified implication study.
(a ->2 (a_|_ ->2 b)) = (((a ^ b_|_) v (a_|_ ^ b_|_)) v b)
Theorem	u3lem7 756	Lemma for unified implication study.
(a ->3 (a_|_ ->3 b)) = (a_|_ v ((a ^ b) v (a ^ b_|_)))
Theorem	u2lem7n 757	Lemma for unified implication study.
(a ->2 (a_|_ ->2 b))_|_ = (((a v b) ^ (a_|_ v b)) ^ b_|_)
Theorem	u1lem8 758	Lemma used in study of orthoarguesian law.
((a ->1 b) ^ (a_|_ ->1 b)) = ((a ^ b) v (a_|_ ^ b))
Theorem	u1lem9a 759	Lemma used in study of orthoarguesian law.
(a_|_ ->1 b)_|_ =< a_|_
Theorem	u1lem9b 760	Lemma used in study of orthoarguesian law.
a_|_ =< (a ->1 b)
Theorem	u1lem9ab 761	Lemma used in study of orthoarguesian law.
(a_|_ ->1 b)_|_ =< (a ->1 b)
Theorem	u1lem11 762	Lemma used in study of orthoarguesian law.
((a_|_ ->1 b) ->1 b) = (a ->1 b)
Theorem	u1lem12 763	Lemma used in study of orthoarguesian law.
((a ->1 b) ->1 b) = (a_|_ ->1 b)
Theorem	u2lem8 764	Lemma for unified implication study.
(a_|_ ->2 (a ->2 (a_|_ ->2 b))) = (a ->2 (a_|_ ->2 b))
Theorem	u3lem8 765	Lemma for unified implication study.
(a_|_ ->3 (a ->3 (a_|_ ->3 b))) = 1
Theorem	u3lem9 766	Lemma for unified implication study.
(a ->3 (a ->3 (a_|_ ->3 b))) = (a ->3 (a_|_ ->3 b))
Theorem	u3lem10 767	Lemma for unified implication study.
(a ->3 (a_|_ ^ (a v b))) = a_|_
Theorem	u3lem11 768	Lemma for unified implication study.
(a ->3 (b_|_ ^ (a v b))) = (a ->3 b_|_)
Theorem	u3lem11a 769	Lemma for unified implication study.
(a ->3 ((b ->3 a) ->3 (a ->3 b))_|_) = (a ->3 b_|_)
Theorem	u3lem12 770	Lemma for unified implication study.
(a ->3 (a ->3 b_|_))_|_ = (a ^ b)
Theorem	u3lem13a 771	Lemma for unified implication study.
(a ->3 (a ->3 b_|_)_|_) = (a ->1 b)
Theorem	u3lem13b 772	Lemma for unified implication study.
((a ->3 b_|_) ->3 a_|_) = (a ->1 b)
Theorem	u3lem14a 773	Lemma for unified implication study.
(a ->3 ((b ->3 a_|_) ->3 b_|_)) = (a ->3 (b ->3 a))
Theorem	u3lem14aa 774	Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 ((b ->3 a_|_) ->3 b_|_))) = 1
Theorem	u3lem14aa2 775	Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 (b ->3 (b ->3 a_|_)_|_))) = 1
Theorem	u3lem14mp 776	Used to prove ->1 modus ponens rule in ->3 system.
((a ->3 b_|_)_|_ ->3 (a ->3 (a ->3 b))) = 1
Theorem	u3lem15 777	Lemma for Kalmbach implication.
((a ->3 b) ^ (a v b)) = ((a_|_ v b) ^ (a v (a_|_ ^ b)))