[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 8 of 13)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 701-800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremu1lemc4 701 Lemma for Sasaki implication study. (Contributed by NM, 24-Dec-1997.)
a C b       (a1 b) = (ab)
 
Theoremu2lemc4 702 Lemma for Dishkant implication study. (Contributed by NM, 24-Dec-1997.)
a C b       (a2 b) = (ab)
 
Theoremu3lemc4 703 Lemma for Kalmbach implication study. (Contributed by NM, 24-Dec-1997.)
a C b       (a3 b) = (ab)
 
Theoremu4lemc4 704 Lemma for non-tollens implication study. (Contributed by NM, 24-Dec-1997.)
a C b       (a4 b) = (ab)
 
Theoremu5lemc4 705 Lemma for relevance implication study. (Contributed by NM, 24-Dec-1997.)
a C b       (a5 b) = (ab)
 
Theoremu1lemc6 706 Commutation theorem for Sasaki implication. (Contributed by NM, 19-Mar-1999.)
(a1 b) C (a1 b)
 
Theoremcomi12 707 Commutation theorem for 1 and 2 . (Contributed by NM, 5-Jul-2000.)
(a1 b) C (c2 a)
 
Theoremi1com 708 Commutation expressed with 1 . (Contributed by NM, 1-Dec-1999.)
b ≤ (a1 b)       a C b
 
Theoremcomi1 709 Commutation expressed with 1 . (Contributed by NM, 1-Dec-1999.)
a C b       b ≤ (a1 b)
 
Theoremu1lemle1 710 L.e. to Sasaki implication. (Contributed by NM, 11-Jan-1998.)
ab       (a1 b) = 1
 
Theoremu2lemle1 711 L.e. to Dishkant implication. (Contributed by NM, 11-Jan-1998.)
ab       (a2 b) = 1
 
Theoremu3lemle1 712 L.e. to Kalmbach implication. (Contributed by NM, 11-Jan-1998.)
ab       (a3 b) = 1
 
Theoremu4lemle1 713 L.e. to non-tollens implication. (Contributed by NM, 11-Jan-1998.)
ab       (a4 b) = 1
 
Theoremu5lemle1 714 L.e. to relevance implication. (Contributed by NM, 11-Jan-1998.)
ab       (a5 b) = 1
 
Theoremu1lemle2 715 Sasaki implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a1 b) = 1       ab
 
Theoremu2lemle2 716 Dishkant implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a2 b) = 1       ab
 
Theoremu3lemle2 717 Kalmbach implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a3 b) = 1       ab
 
Theoremu4lemle2 718 Non-tollens implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a4 b) = 1       ab
 
Theoremu5lemle2 719 Relevance implication to l.e. (Contributed by NM, 11-Jan-1998.)
(a5 b) = 1       ab
 
Theoremu1lembi 720 Sasaki implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a1 b) ∩ (b1 a)) = (ab)
 
Theoremu2lembi 721 Dishkant implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a2 b) ∩ (b2 a)) = (ab)
 
Theoremi2bi 722 Dishkant implication expressed with biconditional. (Contributed by NM, 20-Nov-1998.)
(a2 b) = (b ∪ (ab))
 
Theoremu3lembi 723 Kalmbach implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a3 b) ∩ (b3 a)) = (ab)
 
Theoremu4lembi 724 Non-tollens implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a4 b) ∩ (b4 a)) = (ab)
 
Theoremu5lembi 725 Relevance implication and biconditional. (Contributed by NM, 17-Jan-1998.)
((a5 b) ∩ (b5 a)) = (ab)
 
Theoremu12lembi 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.)
((a1 b) ∩ (b2 a)) = (ab)
 
Theoremu21lembi 727 Dishkant/Sasaki implication and biconditional. (Contributed by NM, 3-Mar-2000.)
((a2 b) ∩ (b1 a)) = (ab)
 
Theoremublemc1 728 Commutation theorem for biimplication. (Contributed by NM, 19-Sep-1998.)
a C (ab)
 
Theoremublemc2 729 Commutation theorem for biimplication. (Contributed by NM, 19-Sep-1998.)
b C (ab)
 
0.3.7  Some proofs contributed by Josiah Burroughs
 
Theoremu1lemn1b 730 This theorem continues the line of proofs such as u1lemnaa 640, ud1lem0b 256, u1lemnanb 655, etc. (Contributed by Josiah Burroughs, 26-May-2004.)
(a1 b) = ((a1 b)1 b)
 
Theoremu1lem3var1 731 A 3-variable formula. (Contributed by Josiah Burroughs, 26-May-2004.)
(((a1 c) ∩ (b1 c)) ∪ (((a1 c)1 c) ∩ ((b1 c)1 c))) = 1
 
Theoremoi3oa3lem1 732 An attempt at the OA3 conjecture, which is true if (ab) = 1. (Contributed by Josiah Burroughs, 27-May-2004.)
1 = (ba)       (((a1 c) ∩ (b1 c)) ∪ (ab)) = 1
 
Theoremoi3oa3 733 An attempt at the OA3 conjecture, which is true if (ab) = 1. (Contributed by Josiah Burroughs, 27-May-2004.)
1 = (ba)       (((a1 c) ∩ (b1 c)) ∪ ((((a1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ (ab))) →1 c) ∩ (((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ (ab))) →1 c))) = 1
 
0.3.8  More lemmas for unified implication
 
Theoremu1lem1 734 Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a1 b) →1 a) = a
 
Theoremu2lem1 735 Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a2 b) →2 a) = a
 
Theoremu3lem1 736 Lemma for unified implication study. (Contributed by NM, 14-Dec-1997.)
((a3 b) →3 a) = ((ab) ∩ (ab ))
 
Theoremu4lem1 737 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b) →4 a) = ((((ab) ∪ (ab )) ∪ a ) ∩ ((ab) ∩ (ab )))
 
Theoremu5lem1 738 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b) →5 a) = ((ab) ∩ (ab ))
 
Theoremu1lem1n 739 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a1 b) →1 a) = a
 
Theoremu2lem1n 740 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a2 b) →2 a) = a
 
Theoremu3lem1n 741 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a3 b) →3 a) = ((ab) ∪ (ab ))
 
Theoremu4lem1n 742 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a4 b) →4 a) = ((((ab) ∩ (ab )) ∩ a) ∪ ((ab) ∪ (ab )))
 
Theoremu5lem1n 743 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
((a5 b) →5 a) = ((ab) ∪ (ab ))
 
Theoremu1lem2 744 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
(((a1 b) →1 a) →1 a) = 1
 
Theoremu2lem2 745 Lemma for unified implication study. (Contributed by NM, 16-Dec-1997.)
(((a2 b) →2 a) →2 a) = 1
 
Theoremu3lem2 746 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a3 b) →3 a) →3 a) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu4lem2 747 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a4 b) →4 a) →4 a) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu5lem2 748 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(((a5 b) →5 a) →5 a) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu1lem3 749 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a1 (b1 a)) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu2lem3 750 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a2 (b2 a)) = 1
 
Theoremu3lem3 751 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a3 (b3 a)) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu4lem3 752 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a4 (b4 a)) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu5lem3 753 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a5 (b5 a)) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu3lem3n 754 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a3 (b3 a)) = (a ∩ ((ab) ∩ (ab )))
 
Theoremu4lem3n 755 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a4 (b4 a)) = (a ∩ ((ab) ∩ (ab )))
 
Theoremu5lem3n 756 Lemma for unified implication study. (Contributed by NM, 17-Dec-1997.)
(a5 (b5 a)) = (a ∩ ((ab) ∩ (ab )))
 
Theoremu1lem4 757 Lemma for unified implication study. (Contributed by NM, 11-Jan-1998.)
(a1 (a1 (b1 a))) = (a1 (b1 a))
 
Theoremu3lem4 758 Lemma for unified implication study. (Contributed by NM, 21-Jan-1998.)
(a3 (a3 (b3 a))) = 1
 
Theoremu4lem4 759 Lemma for unified implication study. (Contributed by NM, 18-Dec-1997.)
(a4 (a4 (b4 a))) = (a4 (b4 a))
 
Theoremu5lem4 760 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a5 (a5 (b5 a))) = (a5 (b5 a))
 
Theoremu1lem5 761 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a1 (a1 b)) = (a1 b)
 
Theoremu2lem5 762 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a2 (a2 b)) = (a2 b)
 
Theoremu3lem5 763 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a3 (a3 b)) = (ab)
 
Theoremu4lem5 764 Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)
(a4 (a4 b)) = ((ab ) ∪ b)
 
Theoremu5lem5 765 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a5 (a5 b)) = (a ∪ (ab))
 
Theoremu4lem5n 766 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a4 (a4 b)) = ((ab) ∩ b )
 
Theoremu3lem6 767 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a3 (a3 (a3 b))) = (a3 (a3 b))
 
Theoremu4lem6 768 Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)
(a4 (a4 (a4 b))) = (a4 b)
 
Theoremu5lem6 769 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
(a5 (a5 (a5 b))) = (a5 (a5 b))
 
Theoremu24lem 770 Lemma for unified implication study. (Contributed by NM, 20-Dec-1997.)
((a2 b) ∩ (a4 b)) = (a5 b)
 
Theoremu12lem 771 Implication lemma. (Contributed by NM, 17-Nov-1998.)
((a1 b) ∪ (a2 b)) = (a0 b)
 
Theoremu1lem7 772 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a1 (a1 b)) = 1
 
Theoremu2lem7 773 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a2 (a2 b)) = (((ab ) ∪ (ab )) ∪ b)
 
Theoremu3lem7 774 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a3 (a3 b)) = (a ∪ ((ab) ∪ (ab )))
 
Theoremu2lem7n 775 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a2 (a2 b)) = (((ab) ∩ (ab)) ∩ b )
 
Theoremu1lem8 776 Lemma used in study of orthoarguesian law. (Contributed by NM, 27-Dec-1998.)
((a1 b) ∩ (a1 b)) = ((ab) ∪ (ab))
 
Theoremu1lem9a 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.)
(a1 b)a
 
Theoremu1lem9b 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 ≤ (a1 b)
 
Theoremu1lem9ab 779 Lemma used in study of orthoarguesian law. (Contributed by NM, 27-Dec-1998.)
(a1 b) ≤ (a1 b)
 
Theoremu1lem11 780 Lemma used in study of orthoarguesian law. (Contributed by NM, 28-Dec-1998.)
((a1 b) →1 b) = (a1 b)
 
Theoremu1lem12 781 Lemma used in study of orthoarguesian law. Equation 4.12 of [MegPav2000] p. 23. (Contributed by NM, 28-Dec-1998.)
((a1 b) →1 b) = (a1 b)
 
Theoremu2lem8 782 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a2 (a2 (a2 b))) = (a2 (a2 b))
 
Theoremu3lem8 783 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a3 (a3 (a3 b))) = 1
 
Theoremu3lem9 784 Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
(a3 (a3 (a3 b))) = (a3 (a3 b))
 
Theoremu3lem10 785 Lemma for unified implication study. (Contributed by NM, 17-Jan-1998.)
(a3 (a ∩ (ab))) = a
 
Theoremu3lem11 786 Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a3 (b ∩ (ab))) = (a3 b )
 
Theoremu3lem11a 787 Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a3 ((b3 a) →3 (a3 b)) ) = (a3 b )
 
Theoremu3lem12 788 Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a3 (a3 b )) = (ab)
 
Theoremu3lem13a 789 Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
(a3 (a3 b ) ) = (a1 b)
 
Theoremu3lem13b 790 Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)
((a3 b ) →3 a ) = (a1 b)
 
Theoremu3lem14a 791 Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)
(a3 ((b3 a ) →3 b )) = (a3 (b3 a))
 
Theoremu3lem14aa 792 Used to prove 1 "add antecedent" rule in 3 system. (Contributed by NM, 19-Jan-1998.)
(a3 (a3 ((b3 a ) →3 b ))) = 1
 
Theoremu3lem14aa2 793 Used to prove 1 "add antecedent" rule in 3 system. (Contributed by NM, 19-Jan-1998.)
(a3 (a3 (b3 (b3 a ) ))) = 1
 
Theoremu3lem14mp 794 Used to prove 1 modus ponens rule in 3 system. (Contributed by NM, 19-Jan-1998.)
((a3 b )3 (a3 (a3 b))) = 1
 
Theoremu3lem15 795 Lemma for Kalmbach implication. (Contributed by NM, 7-Aug-2001.)
((a3 b) ∩ (ab)) = ((ab) ∩ (a ∪ (ab)))
 
Theoremu3lemax4 796 Possible axiom for Kalmbach implication system. (Contributed by NM, 21-Jan-1998.)
((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((c3 (c3 a)) →3 (c3 (c3 b))))))) = 1
 
Theoremu3lemax5 797 Possible axiom for Kalmbach implication system. (Contributed by NM, 23-Jan-1998.)
((a3 b) →3 ((a3 b) →3 ((b3 a) →3 ((b3 a) →3 ((b3 c) →3 ((b3 c) →3 ((c3 b) →3 ((c3 b) →3 (a3 c))))))))) = 1
 
Theorembi1o1a 798 Equivalence to biconditional. (Contributed by NM, 5-Jul-2000.)
(ab) = ((a1 (ab)) ∩ ((ab) →1 a))
 
Theorembiao 799 Equivalence to biconditional. (Contributed by NM, 8-Jul-2000.)
(ab) = ((ab) ≡ (ab))
 
Theoremi2i1i1 800 Equivalence to 2 . (Contributed by NM, 5-Jul-2000.)
(a2 b) = ((a1 (ab)) ∩ ((ab) →1 b))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
  Copyright terms: Public domain < Previous  Next >