HomeHome Intuitionistic Logic Explorer
Theorem List (p. 9 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

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

Theorem List for Intuitionistic Logic Explorer - 801-900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempm4.62 801 Theorem *4.62 of [WhiteheadRussell] p. 120.
 
Theorempm4.66 802 Theorem *4.66 of [WhiteheadRussell] p. 120.
 
Theoremianor 803 Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 13-May-2011.)
 
Theoremanor 804 Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (The proof was shortened by Wolf Lammen, 3-Nov-2012.)
 
TheoremioranOLD 805 Obsolete proof of ioran 645 as of 28-Sep-2014.
 
Theoremoibabs 806 Absorption of disjunction into equivalence. (The proof was shortened by Wolf Lammen, 3-Nov-2013.)
 
Theorempm4.52 807 Theorem *4.52 of [WhiteheadRussell] p. 120. (The proof was shortened by Wolf Lammen, 5-Nov-2012.)
 
Theorempm4.53 808 Theorem *4.53 of [WhiteheadRussell] p. 120.
 
Theorempm4.54 809 Theorem *4.54 of [WhiteheadRussell] p. 120. (The proof was shortened by Wolf Lammen, 5-Nov-2012.)
 
Theorempm4.54OLD 810 Obsolete proof of pm4.54 809 as of 28-Sep-2014.
 
Theorempm4.55 811 Theorem *4.55 of [WhiteheadRussell] p. 120.
 
Theorempm4.56 812 Theorem *4.56 of [WhiteheadRussell] p. 120.
 
Theoremoran 813 Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 7-May-2011.)
 
Theorempm4.57 814 Theorem *4.57 of [WhiteheadRussell] p. 120.
 
Theorempm3.11 815 Theorem *3.11 of [WhiteheadRussell] p. 111.
 
Theorempm3.12 816 Theorem *3.12 of [WhiteheadRussell] p. 111.
 
Theorempm3.13 817 Theorem *3.13 of [WhiteheadRussell] p. 111.
 
Theorempm4.78 818 Theorem *4.78 of [WhiteheadRussell] p. 121. (The proof was shortened by Wolf Lammen, 19-Nov-2012.)
 
Theorempm4.79 819 Theorem *4.79 of [WhiteheadRussell] p. 121. (The proof was shortened by Wolf Lammen, 27-Jun-2013.)
 
Theorempm5.17 820 Theorem *5.17 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 3-Jan-2013.)
 
Theoremorimdi 821 Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
 
Theorempm2.85 822 Theorem *2.85 of [WhiteheadRussell] p. 108. (The proof was shortened by Wolf Lammen, 5-Jan-2013.)
 
Theoremxor 823 Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 22-Jan-2013.)
 
Theoremxor2 824 Two ways to express "exclusive or." (The proof was shortened by Wolf Lammen, 24-Jan-2013.)
 
Theoremdfbi3 825 An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 3-Nov-2013.)
 
Theorempm5.24 826 Theorem *5.24 of [WhiteheadRussell] p. 124.
 
TheoremjcabOLD 827 Obsolete proof of jcab 517 as of 27-Nov-2013
 
Theoremimimorb 828 Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (The proof was shortened by Wolf Lammen, 3-Apr-2013.)
 
Theorempm2.26 829 Theorem *2.26 of [WhiteheadRussell] p. 104. (The proof was shortened by Wolf Lammen, 23-Nov-2012.)
 
Theorempm5.11 830 Theorem *5.11 of [WhiteheadRussell] p. 123.
 
Theorempm5.12 831 Theorem *5.12 of [WhiteheadRussell] p. 123.
 
Theorempm5.14 832 Theorem *5.14 of [WhiteheadRussell] p. 123.
 
Theorempm5.13 833 Theorem *5.13 of [WhiteheadRussell] p. 123. (The proof was shortened by Wolf Lammen, 14-Nov-2012.)
 
Theorempm5.15 834 Theorem *5.15 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 15-Oct-2013.)
 
Theorempm5.55 835 Theorem *5.55 of [WhiteheadRussell] p. 125. (The proof was shortened by Wolf Lammen, 20-Jan-2013.)
 
1.2.8  Miscellaneous theorems of propositional calculus
 
Theorempm5.21nd 836 Eliminate an antecedent implied by each side of a biconditional. (The proof was shortened by Wolf Lammen, 4-Nov-2013.)
   &       &       =>   
 
Theorempm5.35 837 Theorem *5.35 of [WhiteheadRussell] p. 125.
 
Theorempm5.54 838 Theorem *5.54 of [WhiteheadRussell] p. 125. (The proof was shortened by Wolf Lammen, 7-Nov-2013.)
 
Theorembaib 839 Move conjunction outside of biconditional.
   =>   
 
Theorembaibr 840 Move conjunction outside of biconditional.
   =>   
 
Theorempm5.44 841 Theorem *5.44 of [WhiteheadRussell] p. 125.
 
Theorempm5.6 842 Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125.
 
Theoremorcanai 843 Change disjunction in consequent to conjunction in antecedent.
   =>   
 
Theoremintnan 844 Introduction of conjunct inside of a contradiction.
   =>   
 
Theoremintnanr 845 Introduction of conjunct inside of a contradiction.
   =>   
 
Theoremintnand 846 Introduction of conjunct inside of a contradiction.
   =>   
 
Theoremintnanrd 847 Introduction of conjunct inside of a contradiction.
   =>   
 
Theoremmpbiran 848 Detach truth from conjunction in biconditional.
   &       =>   
 
Theoremmpbiran2 849 Detach truth from conjunction in biconditional.
   &       =>   
 
Theoremmpbir2an 850 Detach a conjunction of truths in a biconditional.
   &       &       =>   
 
Theoremmpbi2and 851 Detach a conjunction of truths in a biconditional. (The proof was shortened by Wolf Lammen, 24-Nov-2012.)
   &       &       =>   
 
Theoremmpbir2and 852 Detach a conjunction of truths in a biconditional. (The proof was shortened by Wolf Lammen, 24-Nov-2012.)
   &       &       =>   
 
TheoremmpbiranOLD 853 Obsolete version of mpbiran 848 as of 9-Jan-2015.
   &       =>   
 
Theoremmpbiran2OLD 854 Obsolete version of mpbiran2 849 as of 9-Jan-2015.
   &       =>   
 
Theoremmpbir2anOLD 855 Obsolete version of mpbir2an 850 as of 9-Jan-2015.
   &       &       =>   
 
Theoremmpbi2andOLD 856 Obsolete version of mpbi2and 851 as of 9-Jan-2015.
   &       &       =>   
 
Theoremmpbir2andOLD 857 Obsolete version of mpbir2and 852 as of 9-Jan-2015.
   &       &       =>   
 
Theorempm5.62 858 Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
 
Theorempm5.63 859 Theorem *5.63 of [WhiteheadRussell] p. 125. (The proof was shortened by Wolf Lammen, 25-Dec-2012.)
 
Theorembianfi 860 A wff conjoined with falsehood is false. (The proof was shortened by Wolf Lammen, 26-Nov-2012.)
   =>   
 
Theorembianfd 861 A wff conjoined with falsehood is false. (The proof was shortened by Wolf Lammen, 5-Nov-2013.)
   =>   
 
Theorempm4.43 862 Theorem *4.43 of [WhiteheadRussell] p. 119. (The proof was shortened by Wolf Lammen, 26-Nov-2012.)
 
Theorempm4.82 863 Theorem *4.82 of [WhiteheadRussell] p. 122.
 
Theorempm4.83 864 Theorem *4.83 of [WhiteheadRussell] p. 122.
 
Theorempclem6 865 Negation inferred from embedded conjunct. (The proof was shortened by Wolf Lammen, 25-Nov-2012.)
 
Theorembiantr 866 A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117.
 
Theoremorbidi 867 Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (The proof was shortened by Wolf Lammen, 4-Feb-2013.)
 
Theorembiluk 868 Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96.
 
Theorempm5.7 869 Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 867. (Contributed by Roy F. Longton, 21-Jun-2005.)
 
Theorembigolden 870 Dijkstra-Scholten's Golden Rule for calculational proofs.
 
Theorempm5.71 871 Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
 
Theorempm5.75 872 Theorem *5.75 of [WhiteheadRussell] p. 126. (The proof was shortened by Andrew Salmon, 7-May-2011.) (The proof was shortened by Wolf Lammen, 23-Dec-2012.)
 
Theorembimsc1 873 Removal of conjunct from one side of an equivalence.
 
Theorem4exmid 874 The disjunction of the four possible combinations of two wffs and their negations is always true. (Contributed by David Abernethy, 28-Jan-2014.)
 
Theoremecase2d 875 Deduction for elimination by cases. (The proof was shortened by Wolf Lammen, 22-Dec-2012.)
   &       &       &       =>   
 
Theoremecase3 876 Inference for elimination by cases. (The proof was shortened by Wolf Lammen, 26-Nov-2012.)
   &       &       =>   
 
Theoremecase 877 Inference for elimination by cases.
   &       &       =>   
 
Theoremecase3d 878 Deduction for elimination by cases. (The proof was shortened by Andrew Salmon, 7-May-2011.)
   &       &       =>   
 
Theoremecased 879 Deduction for elimination by cases.
   &       &       =>   
 
Theoremecase3ad 880 Deduction for elimination by cases.
   &       &       =>   
 
Theoremccase 881 Inference for combining cases. (The proof was shortened by Wolf Lammen, 6-Jan-2013.)
   &       &       &       =>   
 
Theoremccased 882 Deduction for combining cases.
   &       &       &       =>   
 
Theoremccase2 883 Inference for combining cases.
   &       &       =>   
 
Theorem4cases 884 Inference eliminating two antecedents from the four possible cases that result from their true/false combinations.
   &       &       &       =>   
 
Theorem4casesdan 885 Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations.
   &       &       &       =>   
 
Theoremniabn 886 Miscellaneous inference relating falsehoods.
   =>   
 
Theoremdedlem0a 887 Lemma for an alternate version of weak deduction theorem. (The proof was shortened by Andrew Salmon, 7-May-2011.) (The proof was shortened by Wolf Lammen, 4-Dec-2012.)
 
Theoremdedlem0b 888 Lemma for an alternate version of weak deduction theorem.
 
Theoremdedlema 889 Lemma for weak deduction theorem. (The proof was shortened by Andrew Salmon, 7-May-2011.)
 
Theoremdedlemb 890 Lemma for weak deduction theorem. (The proof was shortened by Andrew Salmon, 7-May-2011.)
 
Theoremelimh 891 Hypothesis builder for weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
   &       &       =>   
 
Theoremdedt 892 The weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page.
   &       =>   
 
Theoremcon3th 893 Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version of con3 550 demonstrates the use of the weak deduction theorem to derive it from con3i 543.
 
Theoremconsensus 894 The consensus theorem. This theorem and its dual (with and interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term on the left-hand side is redundant. (The proof was shortened by Andrew Salmon, 13-May-2011.) (The proof was shortened by Wolf Lammen, 20-Jan-2013.)
 
Theorempm4.42 895 Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Roy F. Longton, 21-Jun-2005.)
 
Theoremninba 896 Miscellaneous inference relating falsehoods.
   =>   
 
Theoremprlem1 897 A specialized lemma for set theory (to derive the Axiom of Pairing). (The proof was shortened by Andrew Salmon, 13-May-2011.) (The proof was shortened by Wolf Lammen, 5-Jan-2013.)
   &       =>   
 
Theoremprlem2 898 A specialized lemma for set theory (to derive the Axiom of Pairing). (The proof was shortened by Andrew Salmon, 13-May-2011.) (The proof was shortened by Wolf Lammen, 9-Dec-2012.)
 
Theoremoplem1 899 A specialized lemma for set theory (ordered pair theorem). (The proof was shortened by Wolf Lammen, 8-Dec-2012.) (The proof was shortened by Mario Carneiro, 2-Feb-2015.)
   &       &       &       =>   
 
Theoremrnlem 900 Lemma used in construction of real numbers. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)
    < 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-800801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-1914
  Copyright terms: Public domain < Previous  Next >