P. 8 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 701-800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	u1lemc4 701	Lemma for Sasaki implication study. (Contributed by NM, 24-Dec-1997.)
a C b    ⇒   (a →1 b) = (a⊥ ∪ b)
Theorem	u2lemc4 702	Lemma for Dishkant implication study. (Contributed by NM, 24-Dec-1997.)
a C b    ⇒   (a →2 b) = (a⊥ ∪ b)
Theorem	u3lemc4 703	Lemma for Kalmbach implication study. (Contributed by NM, 24-Dec-1997.)
a C b    ⇒   (a →3 b) = (a⊥ ∪ b)
Theorem	u4lemc4 704	Lemma for non-tollens implication study. (Contributed by NM, 24-Dec-1997.)
a C b    ⇒   (a →4 b) = (a⊥ ∪ b)
Theorem	u5lemc4 705	Lemma for relevance implication study. (Contributed by NM, 24-Dec-1997.)
a C b    ⇒   (a →5 b) = (a⊥ ∪ b)
Theorem	u1lemc6 706	Commutation theorem for Sasaki implication. (Contributed by NM, 19-Mar-1999.)
(a →1 b) C (a⊥ →1 b)
Theorem	comi12 707	Commutation theorem for →1 and →2 . (Contributed by NM, 5-Jul-2000.)
(a →1 b) C (c →2 a)
Theorem	i1com 708	Commutation expressed with →1 . (Contributed by NM, 1-Dec-1999.)
b ≤ (a →1 b)    ⇒   a C b
Theorem	comi1 709	Commutation expressed with →1 . (Contributed by NM, 1-Dec-1999.)
a C b    ⇒   b ≤ (a →1 b)
Theorem	u1lemle1 710	L.e. to Sasaki implication. (Contributed by NM, 11-Jan-1998.)
a ≤ b    ⇒   (a →1 b) = 1
Theorem	u2lemle1 711	L.e. to Dishkant implication. (Contributed by NM, 11-Jan-1998.)
a ≤ b    ⇒   (a →2 b) = 1
Theorem	u3lemle1 712	L.e. to Kalmbach implication. (Contributed by NM, 11-Jan-1998.)
a ≤ b    ⇒   (a →3 b) = 1
Theorem	u4lemle1 713	L.e. to non-tollens implication. (Contributed by NM, 11-Jan-1998.)
a ≤ b    ⇒   (a →4 b) = 1
Theorem	u5lemle1 714	L.e. to relevance implication. (Contributed by NM, 11-Jan-1998.)
a ≤ b    ⇒   (a →5 b) = 1
Theorem	u1lemle2 715	Sasaki implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a →1 b) = 1    ⇒   a ≤ b
Theorem	u2lemle2 716	Dishkant implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a →2 b) = 1    ⇒   a ≤ b
Theorem	u3lemle2 717	Kalmbach implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a →3 b) = 1    ⇒   a ≤ b
Theorem	u4lemle2 718	Non-tollens implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a →4 b) = 1    ⇒   a ≤ b
Theorem	u5lemle2 719	Relevance implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a →5 b) = 1    ⇒   a ≤ b
Theorem	u1lembi 720	Sasaki implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a →1 b) ∩ (b →1 a)) = (a ≡ b)
Theorem	u2lembi 721	Dishkant implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a →2 b) ∩ (b →2 a)) = (a ≡ b)
Theorem	i2bi 722	Dishkant implication expressed with biconditional. (Contributed by NM, 20-Nov-1998.)
(a →2 b) = (b ∪ (a ≡ b))
Theorem	u3lembi 723	Kalmbach implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a →3 b) ∩ (b →3 a)) = (a ≡ b)
Theorem	u4lembi 724	Non-tollens implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a →4 b) ∩ (b →4 a)) = (a ≡ b)
Theorem	u5lembi 725	Relevance implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a →5 b) ∩ (b →5 a)) = (a ≡ b)
Theorem	u12lembi 726	Sasaki/Dishkant implication and biconditional. Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 2. (Contributed by NM, 2-Mar-2000.)
((a →1 b) ∩ (b →2 a)) = (a ≡ b)
Theorem	u21lembi 727	Dishkant/Sasaki implication and biconditional. (Contributed by NM, 3-Mar-2000.)
((a →2 b) ∩ (b →1 a)) = (a ≡ b)
Theorem	ublemc1 728	Commutation theorem for biimplication. (Contributed by NM, 19-Sep-1998.)
a C (a ≡ b)
Theorem	ublemc2 729	Commutation theorem for biimplication. (Contributed by NM, 19-Sep-1998.)
b C (a ≡ b)
0.3.7  Some proofs contributed by Josiah Burroughs
Theorem	u1lemn1b 730	This theorem continues the line of proofs such as u1lemnaa 640, ud1lem0b 256, u1lemnanb 655, etc. (Contributed by Josiah Burroughs, 26-May-2004.)
(a →1 b) = ((a →1 b)⊥ →1 b)
Theorem	u1lem3var1 731	A 3-variable formula. (Contributed by Josiah Burroughs, 26-May-2004.)
(((a →1 c) ∩ (b →1 c))⊥ ∪ (((a →1 c)⊥ →1 c) ∩ ((b →1 c)⊥ →1 c))) = 1
Theorem	oi3oa3lem1 732	An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs, 27-May-2004.)
1 = (b ≡ a)    ⇒   (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b)) = 1
Theorem	oi3oa3 733	An attempt at the OA3 conjecture, which is true if (a ≡ b) = 1. (Contributed by Josiah Burroughs, 27-May-2004.)
1 = (b ≡ a)    ⇒   (((a →1 c) ∩ (b →1 c)) ∪ ((((a →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b))) →1 c) ∩ (((b →1 c) ∩ (((a →1 c) ∩ (b →1 c)) ∪ (a ∩ b))) →1 c))) = 1
0.3.8  More lemmas for unified implication
Theorem	u1lem1 734	Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a →1 b) →1 a) = a
Theorem	u2lem1 735	Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a →2 b) →2 a) = a
Theorem	u3lem1 736	Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a →3 b) →3 a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u4lem1 737	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b) →4 a) = ((((a ∩ b) ∪ (a ∩ b⊥ )) ∪ a⊥ ) ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u5lem1 738	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b) →5 a) = ((a ∪ b) ∩ (a ∪ b⊥ ))
Theorem	u1lem1n 739	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →1 b) →1 a)⊥ = a⊥
Theorem	u2lem1n 740	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →2 b) →2 a)⊥ = a⊥
Theorem	u3lem1n 741	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →3 b) →3 a)⊥ = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u4lem1n 742	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →4 b) →4 a)⊥ = ((((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )) ∩ a) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u5lem1n 743	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a →5 b) →5 a)⊥ = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
Theorem	u1lem2 744	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
(((a →1 b) →1 a) →1 a) = 1
Theorem	u2lem2 745	Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
(((a →2 b) →2 a) →2 a) = 1
Theorem	u3lem2 746	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a →3 b) →3 a) →3 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lem2 747	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a →4 b) →4 a) →4 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u5lem2 748	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a →5 b) →5 a) →5 a) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u1lem3 749	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →1 (b →1 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u2lem3 750	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →2 (b →2 a)) = 1
Theorem	u3lem3 751	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →3 (b →3 a)) = (a ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
Theorem	u4lem3 752	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →4 (b →4 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u5lem3 753	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →5 (b →5 a)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u3lem3n 754	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →3 (b →3 a))⊥ = (a⊥ ∩ ((a ∪ b) ∩ (a ∪ b⊥ )))
Theorem	u4lem3n 755	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →4 (b →4 a))⊥ = (a ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	u5lem3n 756	Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a →5 (b →5 a))⊥ = (a ∩ ((a⊥ ∪ b) ∩ (a⊥ ∪ b⊥ )))
Theorem	u1lem4 757	Lemma for unified implication study. (Contributed by NM, 11-Jan-1998.)
(a →1 (a →1 (b →1 a))) = (a →1 (b →1 a))
Theorem	u3lem4 758	Lemma for unified implication study. (Contributed by NM, 21-Jan-1998.)
(a →3 (a →3 (b →3 a))) = 1
Theorem	u4lem4 759	Lemma for unified implication study. (Contributed by NM, 18-Dec-1997.)
(a →4 (a →4 (b →4 a))) = (a →4 (b →4 a))
Theorem	u5lem4 760	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →5 (a →5 (b →5 a))) = (a →5 (b →5 a))
Theorem	u1lem5 761	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a →1 (a →1 b)) = (a →1 b)
Theorem	u2lem5 762	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a →2 (a →2 b)) = (a →2 b)
Theorem	u3lem5 763	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →3 (a →3 b)) = (a⊥ ∪ b)
Theorem	u4lem5 764	Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)
(a →4 (a →4 b)) = ((a⊥ ∩ b⊥ ) ∪ b)
Theorem	u5lem5 765	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a →5 (a →5 b)) = (a⊥ ∪ (a ∩ b))
Theorem	u4lem5n 766	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a →4 (a →4 b))⊥ = ((a ∪ b) ∩ b⊥ )
Theorem	u3lem6 767	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →3 (a →3 (a →3 b))) = (a →3 (a →3 b))
Theorem	u4lem6 768	Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)
(a →4 (a →4 (a →4 b))) = (a →4 b)
Theorem	u5lem6 769	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a →5 (a →5 (a →5 b))) = (a →5 (a →5 b))
Theorem	u24lem 770	Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
((a →2 b) ∩ (a →4 b)) = (a →5 b)
Theorem	u12lem 771	Implication lemma. (Contributed by NM, 17-Nov-1998.)
((a →1 b) ∪ (a →2 b)) = (a →0 b)
Theorem	u1lem7 772	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →1 (a⊥ →1 b)) = 1
Theorem	u2lem7 773	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →2 (a⊥ →2 b)) = (((a ∩ b⊥ ) ∪ (a⊥ ∩ b⊥ )) ∪ b)
Theorem	u3lem7 774	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →3 (a⊥ →3 b)) = (a⊥ ∪ ((a ∩ b) ∪ (a ∩ b⊥ )))
Theorem	u2lem7n 775	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →2 (a⊥ →2 b))⊥ = (((a ∪ b) ∩ (a⊥ ∪ b)) ∩ b⊥ )
Theorem	u1lem8 776	Lemma used in study of orthoarguesian law. (Contributed by NM, 27-Dec-1998.)
((a →1 b) ∩ (a⊥ →1 b)) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	u1lem9a 777	Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the first part of the inequality. (Contributed by NM, 28-Dec-1998.)
(a⊥ →1 b)⊥ ≤ a⊥
Theorem	u1lem9b 778	Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the second part of the inequality. (Contributed by NM, 27-Dec-1998.)
a⊥ ≤ (a →1 b)
Theorem	u1lem9ab 779	Lemma used in study of orthoarguesian law. (Contributed by NM, 27-Dec-1998.)
(a⊥ →1 b)⊥ ≤ (a →1 b)
Theorem	u1lem11 780	Lemma used in study of orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
((a⊥ →1 b) →1 b) = (a →1 b)
Theorem	u1lem12 781	Lemma used in study of orthoarguesian law. Equation 4.12 of [MegPav2000] p. 23. (Contributed by NM, 28-Dec-1998.)
((a →1 b) →1 b) = (a⊥ →1 b)
Theorem	u2lem8 782	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a⊥ →2 (a →2 (a⊥ →2 b))) = (a →2 (a⊥ →2 b))
Theorem	u3lem8 783	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a⊥ →3 (a →3 (a⊥ →3 b))) = 1
Theorem	u3lem9 784	Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a →3 (a →3 (a⊥ →3 b))) = (a →3 (a⊥ →3 b))
Theorem	u3lem10 785	Lemma for unified implication study. (Contributed by NM, 17-Jan-1998.)
(a →3 (a⊥ ∩ (a ∪ b))) = a⊥
Theorem	u3lem11 786	Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a →3 (b⊥ ∩ (a ∪ b))) = (a →3 b⊥ )
Theorem	u3lem11a 787	Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a →3 ((b →3 a) →3 (a →3 b))⊥ ) = (a →3 b⊥ )
Theorem	u3lem12 788	Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a →3 (a →3 b⊥ ))⊥ = (a ∩ b)
Theorem	u3lem13a 789	Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a →3 (a →3 b⊥ )⊥ ) = (a →1 b)
Theorem	u3lem13b 790	Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)
((a →3 b⊥ ) →3 a⊥ ) = (a →1 b)
Theorem	u3lem14a 791	Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)
(a →3 ((b →3 a⊥ ) →3 b⊥ )) = (a →3 (b →3 a))
Theorem	u3lem14aa 792	Used to prove →1 "add antecedent" rule in →3 system. (Contributed by NM, 19-Jan-1998.)
(a →3 (a →3 ((b →3 a⊥ ) →3 b⊥ ))) = 1
Theorem	u3lem14aa2 793	Used to prove →1 "add antecedent" rule in →3 system. (Contributed by NM, 19-Jan-1998.)
(a →3 (a →3 (b →3 (b →3 a⊥ )⊥ ))) = 1
Theorem	u3lem14mp 794	Used to prove →1 modus ponens rule in →3 system. (Contributed by NM, 19-Jan-1998.)
((a →3 b⊥ )⊥ →3 (a →3 (a →3 b))) = 1
Theorem	u3lem15 795	Lemma for Kalmbach implication. (Contributed by NM, 7-Aug-2001.)
((a →3 b) ∩ (a ∪ b)) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b)))
Theorem	u3lemax4 796	Possible axiom for Kalmbach implication system. (Contributed by NM, 21-Jan-1998.)
((a →3 b) →3 ((a →3 b) →3 ((b →3 a) →3 ((b →3 a) →3 ((c →3 (c →3 a)) →3 (c →3 (c →3 b))))))) = 1
Theorem	u3lemax5 797	Possible axiom for Kalmbach implication system. (Contributed by NM, 23-Jan-1998.)
((a →3 b) →3 ((a →3 b) →3 ((b →3 a) →3 ((b →3 a) →3 ((b →3 c) →3 ((b →3 c) →3 ((c →3 b) →3 ((c →3 b) →3 (a →3 c))))))))) = 1
Theorem	bi1o1a 798	Equivalence to biconditional. (Contributed by NM, 5-Jul-2000.)
(a ≡ b) = ((a →1 (a ∩ b)) ∩ ((a ∪ b) →1 a))
Theorem	biao 799	Equivalence to biconditional. (Contributed by NM, 8-Jul-2000.)
(a ≡ b) = ((a ∩ b) ≡ (a ∪ b))
Theorem	i2i1i1 800	Equivalence to →2 . (Contributed by NM, 5-Jul-2000.)
(a →2 b) = ((a →1 (a ∪ b)) ∩ ((a ∪ b) →1 b))