[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 8 of 13) 		< Previous  Next >
Browser slow? Try the
Unicode 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.
a C b   =>   (a ->1 b) = (a' v b)
 
Theoremu2lemc4 702 Lemma for Dishkant implication study.
a C b   =>   (a ->2 b) = (a' v b)
 
Theoremu3lemc4 703 Lemma for Kalmbach implication study.
a C b   =>   (a ->3 b) = (a' v b)
 
Theoremu4lemc4 704 Lemma for non-tollens implication study.
a C b   =>   (a ->4 b) = (a' v b)
 
Theoremu5lemc4 705 Lemma for relevance implication study.
a C b   =>   (a ->5 b) = (a' v b)
 
Theoremu1lemc6 706 Commutation theorem for Sasaki implication.
(a ->1 b) C (a' ->1 b)
 
Theoremcomi12 707 Commutation theorem for ->1 and ->2.
(a ->1 b) C (c ->2 a)
 
Theoremi1com 708 Commutation expressed with ->1.
b =< (a ->1 b)   =>   a C b
 
Theoremcomi1 709 Commutation expressed with ->1.
a C b   =>   b =< (a ->1 b)
 
Theoremu1lemle1 710 L.e. to Sasaki implication.
a =< b   =>   (a ->1 b) = 1
 
Theoremu2lemle1 711 L.e. to Dishkant implication.
a =< b   =>   (a ->2 b) = 1
 
Theoremu3lemle1 712 L.e. to Kalmbach implication.
a =< b   =>   (a ->3 b) = 1
 
Theoremu4lemle1 713 L.e. to non-tollens implication.
a =< b   =>   (a ->4 b) = 1
 
Theoremu5lemle1 714 L.e. to relevance implication.
a =< b   =>   (a ->5 b) = 1
 
Theoremu1lemle2 715 Sasaki implication to l.e.
(a ->1 b) = 1   =>   a =< b
 
Theoremu2lemle2 716 Dishkant implication to l.e.
(a ->2 b) = 1   =>   a =< b
 
Theoremu3lemle2 717 Kalmbach implication to l.e.
(a ->3 b) = 1   =>   a =< b
 
Theoremu4lemle2 718 Non-tollens implication to l.e.
(a ->4 b) = 1   =>   a =< b
 
Theoremu5lemle2 719 Relevance implication to l.e.
(a ->5 b) = 1   =>   a =< b
 
Theoremu1lembi 720 Sasaki implication and biconditional.
((a ->1 b) ^ (b ->1 a)) = (a == b)
 
Theoremu2lembi 721 Dishkant implication and biconditional.
((a ->2 b) ^ (b ->2 a)) = (a == b)
 
Theoremi2bi 722 Dishkant implication expressed with biconditional.
(a ->2 b) = (b v (a == b))
 
Theoremu3lembi 723 Kalmbach implication and biconditional.
((a ->3 b) ^ (b ->3 a)) = (a == b)
 
Theoremu4lembi 724 Non-tollens implication and biconditional.
((a ->4 b) ^ (b ->4 a)) = (a == b)
 
Theoremu5lembi 725 Relevance implication and biconditional.
((a ->5 b) ^ (b ->5 a)) = (a == b)
 
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.
((a ->1 b) ^ (b ->2 a)) = (a == b)
 
Theoremu21lembi 727 Dishkant/Sasaki implication and biconditional.
((a ->2 b) ^ (b ->1 a)) = (a == b)
 
Theoremublemc1 728 Commutation theorem for biimplication.
a C (a == b)
 
Theoremublemc2 729 Commutation theorem for biimplication.
b C (a == b)
 
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-04.)
(a ->1 b) = ((a ->1 b)' ->1 b)
 
Theoremu1lem3var1 731 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
 
Theoremoi3oa3lem1 732 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
 
Theoremoi3oa3 733 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
 
0.3.8  More lemmas for unified implication
 
Theoremu1lem1 734 Lemma for unified implication study.
((a ->1 b) ->1 a) = a
 
Theoremu2lem1 735 Lemma for unified implication study.
((a ->2 b) ->2 a) = a
 
Theoremu3lem1 736 Lemma for unified implication study.
((a ->3 b) ->3 a) = ((a v b) ^ (a v b'))
 
Theoremu4lem1 737 Lemma for unified implication study.
((a ->4 b) ->4 a) = ((((a ^ b) v (a ^ b')) v a') ^ ((a v b) ^ (a v b')))
 
Theoremu5lem1 738 Lemma for unified implication study.
((a ->5 b) ->5 a) = ((a v b) ^ (a v b'))
 
Theoremu1lem1n 739 Lemma for unified implication study.
((a ->1 b) ->1 a)' = a'
 
Theoremu2lem1n 740 Lemma for unified implication study.
((a ->2 b) ->2 a)' = a'
 
Theoremu3lem1n 741 Lemma for unified implication study.
((a ->3 b) ->3 a)' = ((a' ^ b) v (a' ^ b'))
 
Theoremu4lem1n 742 Lemma for unified implication study.
((a ->4 b) ->4 a)' = ((((a' v b) ^ (a' v b')) ^ a) v ((a' ^ b) v (a' ^ b')))
 
Theoremu5lem1n 743 Lemma for unified implication study.
((a ->5 b) ->5 a)' = ((a' ^ b) v (a' ^ b'))
 
Theoremu1lem2 744 Lemma for unified implication study.
(((a ->1 b) ->1 a) ->1 a) = 1
 
Theoremu2lem2 745 Lemma for unified implication study.
(((a ->2 b) ->2 a) ->2 a) = 1
 
Theoremu3lem2 746 Lemma for unified implication study.
(((a ->3 b) ->3 a) ->3 a) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu4lem2 747 Lemma for unified implication study.
(((a ->4 b) ->4 a) ->4 a) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu5lem2 748 Lemma for unified implication study.
(((a ->5 b) ->5 a) ->5 a) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu1lem3 749 Lemma for unified implication study.
(a ->1 (b ->1 a)) = (a' v ((a ^ b) v (a ^ b')))
 
Theoremu2lem3 750 Lemma for unified implication study.
(a ->2 (b ->2 a)) = 1
 
Theoremu3lem3 751 Lemma for unified implication study.
(a ->3 (b ->3 a)) = (a v ((a' ^ b) v (a' ^ b')))
 
Theoremu4lem3 752 Lemma for unified implication study.
(a ->4 (b ->4 a)) = (a' v ((a ^ b) v (a ^ b')))
 
Theoremu5lem3 753 Lemma for unified implication study.
(a ->5 (b ->5 a)) = (a' v ((a ^ b) v (a ^ b')))
 
Theoremu3lem3n 754 Lemma for unified implication study.
(a ->3 (b ->3 a))' = (a' ^ ((a v b) ^ (a v b')))
 
Theoremu4lem3n 755 Lemma for unified implication study.
(a ->4 (b ->4 a))' = (a ^ ((a' v b) ^ (a' v b')))
 
Theoremu5lem3n 756 Lemma for unified implication study.
(a ->5 (b ->5 a))' = (a ^ ((a' v b) ^ (a' v b')))
 
Theoremu1lem4 757 Lemma for unified implication study.
(a ->1 (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))
 
Theoremu3lem4 758 Lemma for unified implication study.
(a ->3 (a ->3 (b ->3 a))) = 1
 
Theoremu4lem4 759 Lemma for unified implication study.
(a ->4 (a ->4 (b ->4 a))) = (a ->4 (b ->4 a))
 
Theoremu5lem4 760 Lemma for unified implication study.
(a ->5 (a ->5 (b ->5 a))) = (a ->5 (b ->5 a))
 
Theoremu1lem5 761 Lemma for unified implication study.
(a ->1 (a ->1 b)) = (a ->1 b)
 
Theoremu2lem5 762 Lemma for unified implication study.
(a ->2 (a ->2 b)) = (a ->2 b)
 
Theoremu3lem5 763 Lemma for unified implication study.
(a ->3 (a ->3 b)) = (a' v b)
 
Theoremu4lem5 764 Lemma for unified implication study.
(a ->4 (a ->4 b)) = ((a' ^ b') v b)
 
Theoremu5lem5 765 Lemma for unified implication study.
(a ->5 (a ->5 b)) = (a' v (a ^ b))
 
Theoremu4lem5n 766 Lemma for unified implication study.
(a ->4 (a ->4 b))' = ((a v b) ^ b')
 
Theoremu3lem6 767 Lemma for unified implication study.
(a ->3 (a ->3 (a ->3 b))) = (a ->3 (a ->3 b))
 
Theoremu4lem6 768 Lemma for unified implication study.
(a ->4 (a ->4 (a ->4 b))) = (a ->4 b)
 
Theoremu5lem6 769 Lemma for unified implication study.
(a ->5 (a ->5 (a ->5 b))) = (a ->5 (a ->5 b))
 
Theoremu24lem 770 Lemma for unified implication study.
((a ->2 b) ^ (a ->4 b)) = (a ->5 b)
 
Theoremu12lem 771 Implication lemma.
((a ->1 b) v (a ->2 b)) = (a ->0 b)
 
Theoremu1lem7 772 Lemma for unified implication study.
(a ->1 (a' ->1 b)) = 1
 
Theoremu2lem7 773 Lemma for unified implication study.
(a ->2 (a' ->2 b)) = (((a ^ b') v (a' ^ b')) v b)
 
Theoremu3lem7 774 Lemma for unified implication study.
(a ->3 (a' ->3 b)) = (a' v ((a ^ b) v (a ^ b')))
 
Theoremu2lem7n 775 Lemma for unified implication study.
(a ->2 (a' ->2 b))' = (((a v b) ^ (a' v b)) ^ b')
 
Theoremu1lem8 776 Lemma used in study of orthoarguesian law.
((a ->1 b) ^ (a' ->1 b)) = ((a ^ b) v (a' ^ b))
 
Theoremu1lem9a 777 Lemma used in study of orthoarguesian law. Equation 4.11 of [MegPav2000] p. 23. This is the first part of the inequality.
(a' ->1 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.
a' =< (a ->1 b)
 
Theoremu1lem9ab 779 Lemma used in study of orthoarguesian law.
(a' ->1 b)' =< (a ->1 b)
 
Theoremu1lem11 780 Lemma used in study of orthoarguesian law.
((a' ->1 b) ->1 b) = (a ->1 b)
 
Theoremu1lem12 781 Lemma used in study of orthoarguesian law. Equation 4.12 of [MegPav2000] p. 23.
((a ->1 b) ->1 b) = (a' ->1 b)
 
Theoremu2lem8 782 Lemma for unified implication study.
(a' ->2 (a ->2 (a' ->2 b))) = (a ->2 (a' ->2 b))
 
Theoremu3lem8 783 Lemma for unified implication study.
(a' ->3 (a ->3 (a' ->3 b))) = 1
 
Theoremu3lem9 784 Lemma for unified implication study.
(a ->3 (a ->3 (a' ->3 b))) = (a ->3 (a' ->3 b))
 
Theoremu3lem10 785 Lemma for unified implication study.
(a ->3 (a' ^ (a v b))) = a'
 
Theoremu3lem11 786 Lemma for unified implication study.
(a ->3 (b' ^ (a v b))) = (a ->3 b')
 
Theoremu3lem11a 787 Lemma for unified implication study.
(a ->3 ((b ->3 a) ->3 (a ->3 b))') = (a ->3 b')
 
Theoremu3lem12 788 Lemma for unified implication study.
(a ->3 (a ->3 b'))' = (a ^ b)
 
Theoremu3lem13a 789 Lemma for unified implication study.
(a ->3 (a ->3 b')') = (a ->1 b)
 
Theoremu3lem13b 790 Lemma for unified implication study.
((a ->3 b') ->3 a') = (a ->1 b)
 
Theoremu3lem14a 791 Lemma for unified implication study.
(a ->3 ((b ->3 a') ->3 b')) = (a ->3 (b ->3 a))
 
Theoremu3lem14aa 792 Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 ((b ->3 a') ->3 b'))) = 1
 
Theoremu3lem14aa2 793 Used to prove ->1 "add antecedent" rule in ->3 system.
(a ->3 (a ->3 (b ->3 (b ->3 a')'))) = 1
 
Theoremu3lem14mp 794 Used to prove ->1 modus ponens rule in ->3 system.
((a ->3 b')' ->3 (a ->3 (a ->3 b))) = 1
 
Theoremu3lem15 795 Lemma for Kalmbach implication.
((a ->3 b) ^ (a v b)) = ((a' v b) ^ (a v (a' ^ b)))
 
Theoremu3lemax4 796 Possible axiom for Kalmbach implication system.
((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
 
Theoremu3lemax5 797 Possible axiom for Kalmbach implication system.
((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
 
Theorembi1o1a 798 Equivalence to biconditional.
(a == b) = ((a ->1 (a ^ b)) ^ ((a v b) ->1 a))
 
Theorembiao 799 Equivalence to biconditional.
(a == b) = ((a ^ b) == (a v b))
 
Theoremi2i1i1 800 Equivalence to ->2.
(a ->2 b) = ((a ->1 (a v b)) ^ ((a v b) ->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-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215
  Copyright terms: Public domain < Previous  Next >