Home New Foundations ExplorerTheorem List (p. 9 of 64) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 801-900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremanandi 801 Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)

Theoremanandir 802 Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)

Theoremanandis 803 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Theoremanandirs 804 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Theoremimpbida 805 Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)

Theorempm3.48 806 Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)

Theorempm3.45 807 Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)

Theoremim2anan9 808 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)

Theoremim2anan9r 809 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)

Theoremanim12dan 810 Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)

Theoremorim12d 811 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)

Theoremorim1d 812 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Theoremorim2d 813 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Theoremorim2 814 Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)

Theorempm2.38 815 Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)

Theorempm2.36 816 Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)

Theorempm2.37 817 Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)

Theorempm2.73 818 Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)

Theorempm2.74 819 Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Theoremorimdi 820 Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)

Theorempm2.76 821 Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)

Theorempm2.75 822 Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)

Theorempm2.8 823 Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Theorempm2.81 824 Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)

Theorempm2.82 825 Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)

Theorempm2.85 826 Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Theorempm3.2ni 827 Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)

Theoremorabs 828 Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)

Theoremoranabs 829 Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)

Theorempm5.1 830 Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)

Theorempm5.21 831 Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.)

Theorempm3.43 832 Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)

Theoremjcab 833 Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)

Theoremordi 834 Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.)

Theoremordir 835 Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)

Theorempm4.76 836 Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)

Theoremandi 837 Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

Theoremandir 838 Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

Theoremorddi 839 Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)

Theoremanddi 840 Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

Theorempm4.39 841 Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)

Theorempm4.38 842 Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)

Theorembi2anan9 843 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Theorembi2anan9r 844 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)

Theorembi2bian9 845 Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)

Theorempm4.72 846 Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)

Theoremimimorb 847 Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)

Theorempm5.33 848 Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)

Theorempm5.36 849 Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)

Theorembianabs 850 Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)

Theoremoibabs 851 Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)

Theorempm3.24 852 Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theorempm2.26 853 Theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Theorempm5.11 854 Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)

Theorempm5.12 855 Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)

Theorempm5.14 856 Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)

Theorempm5.13 857 Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)

Theorempm5.17 858 Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)

Theorempm5.15 859 Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)

Theorempm5.16 860 Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)

Theoremxor 861 Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)

Theoremnbi2 862 Two ways to express "exclusive or." (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)

Theoremdfbi3 863 An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)

Theorempm5.24 864 Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)

Theoremxordi 865 Conjunction distributes over exclusive-or, using to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. (Contributed by NM, 3-Oct-2008.)

Theorembiort 866 A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.)

Theorempm5.55 867 Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)

1.2.7  Miscellaneous theorems of propositional calculus

Theorempm5.21nd 868 Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)

Theorempm5.35 869 Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)

Theorempm5.54 870 Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)

Theorembaib 871 Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

Theorembaibr 872 Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)

Theoremrbaib 873 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Theoremrbaibr 874 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Theorembaibd 875 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Theoremrbaibd 876 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Theorempm5.44 877 Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)

Theorempm5.6 878 Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)

Theoremorcanai 879 Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)

Theoremintnan 880 Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Theoremintnanr 881 Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)

Theoremintnand 882 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Theoremintnanrd 883 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Theoremmpbiran 884 Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)

Theoremmpbiran2 885 Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Theoremmpbir2an 886 Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)

Theoremmpbi2and 887 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theoremmpbir2and 888 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Theorempm5.62 889 Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)

Theorempm5.63 890 Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)

Theorembianfi 891 A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)

Theorembianfd 892 A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)

Theorempm4.43 893 Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)

Theorempm4.82 894 Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)

Theorempm4.83 895 Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)

Theorempclem6 896 Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)

Theorembiantr 897 A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)

Theoremorbidi 898 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. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.)

Theorembiluk 899 Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)

Theorempm5.7 900 Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 898. (Contributed by Roy F. Longton, 21-Jun-2005.)

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-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >