HomeHome Intuitionistic Logic Explorer
Theorem List (p. 9 of 21)
< 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.55dc 801 Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)
DECID DECID
 
Theoremmpbiran 802 Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
   &       =>   
 
Theoremmpbiran2 803 Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
   &       =>   
 
Theoremmpbir2an 804 Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)
   &       &       =>   
 
Theoremmpbi2and 805 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
   &       &       =>   
 
Theoremmpbir2and 806 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
   &       &       =>   
 
TheoremmpbiranOLD 807 Obsolete version of mpbiran 802 as of 9-Jan-2015. (Contributed by NM, 27-Feb-1996.)
   &       =>   
 
Theoremmpbiran2OLD 808 Obsolete version of mpbiran2 803 as of 9-Jan-2015. (Contributed by NM, 22-Feb-1996.)
   &       =>   
 
Theoremmpbir2anOLD 809 Obsolete version of mpbir2an 804 as of 9-Jan-2015. (Contributed by NM, 10-May-2005.)
   &       &       =>   
 
Theoremmpbi2andOLD 810 Obsolete version of mpbi2and 805 as of 9-Jan-2015. (Contributed by NM, 6-Nov-2011.) (Revised by NM, 24-Nov-2012.)
   &       &       =>   
 
Theoremmpbir2andOLD 811 Obsolete version of mpbir2and 806 as of 9-Jan-2015. (Contributed by NM, 6-Nov-2011.) (Revised by NM, 24-Nov-2012.)
   &       &       =>   
 
Theorempm5.62dc 812 Theorem *5.62 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
DECID
 
Theorempm5.63dc 813 Theorem *5.63 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
DECID
 
Theorembianfi 814 A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
   =>   
 
Theorembianfd 815 A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
   =>   
 
Theorempm4.43 816 Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
 
Theorempm4.82 817 Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.83dc 818 Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 733, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
DECID
 
Theorembiantr 819 A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
 
Theoremorbididc 820 Disjunction distributes over the biconditional, for a decidable proposition. Based on 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 Jim Kingdon, 2-Apr-2018.)
DECID
 
Theorempm5.7dc 821 Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 820. (Contributed by Jim Kingdon, 2-Apr-2018.)
DECID
 
Theorembigolden 822 Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
 
Theoremanordc 823 Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120, but where the propositions are decidable. The forward direction, pm3.1 648, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.)
DECID DECID
 
Theorempm3.11dc 824 Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 648, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
DECID DECID
 
Theorempm3.12dc 825 Theorem *3.12 of [WhiteheadRussell] p. 111, but for decidable propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
DECID DECID
 
Theorempm3.13dc 826 Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 647, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
DECID DECID
 
Theoremdn1dc 827 DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
DECID DECID DECID DECID
 
Theorempm5.71dc 828 Decidable proposition version of theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) (Modified for decidability by Jim Kingdon, 19-Apr-2018.)
DECID
 
Theorempm5.75 829 Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.)
 
Theorembimsc1 830 Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
 
Theoremccase 831 Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
   &       &       &       =>   
 
Theoremccased 832 Deduction for combining cases. (Contributed by NM, 9-May-2004.)
   &       &       &       =>   
 
Theoremccase2 833 Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
   &       &       =>   
 
Theoremniabn 834 Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
   =>   
 
Theoremninba 835 Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
   =>   
 
Theoremprlem1 836 A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
   &       =>   
 
Theoremprlem2 837 A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
 
Theoremoplem1 838 A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
   &       &       &       =>   
 
Theoremrnlem 839 Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
 
1.2.10  Abbreviated conjunction and disjunction of three wff's
 
Syntaxw3o 840 Extend wff definition to include 3-way disjunction ('or').
 
Syntaxw3a 841 Extend wff definition to include 3-way conjunction ('and').
 
Definitiondf-3or 842 Define disjunction ('or') of 3 wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 661. (Contributed by NM, 8-Apr-1994.)
 
Definitiondf-3an 843 Define conjunction ('and') of 3 wff.s. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 379. (Contributed by NM, 8-Apr-1994.)
 
Theorem3orass 844 Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
 
Theorem3anass 845 Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
 
Theorem3anrot 846 Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
 
Theorem3orrot 847 Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
 
Theorem3ancoma 848 Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theorem3ancomb 849 Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theorem3orcomb 850 Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
 
Theorem3anrev 851 Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theorem3ioran 852 Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
 
Theorem3simpa 853 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theorem3simpb 854 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theorem3simpc 855 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
 
Theoremsimp1 856 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theoremsimp2 857 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theoremsimp3 858 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
 
Theoremsimpl1 859 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpl2 860 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpl3 861 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr1 862 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr2 863 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimpr3 864 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
 
Theoremsimp1i 865 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
   =>   
 
Theoremsimp2i 866 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
   =>   
 
Theoremsimp3i 867 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
   =>   
 
Theoremsimp1d 868 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
   =>   
 
Theoremsimp2d 869 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
   =>   
 
Theoremsimp3d 870 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
   =>   
 
Theoremsimp1bi 871 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theoremsimp2bi 872 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theoremsimp3bi 873 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   =>   
 
Theorem3adant1 874 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
   =>   
 
Theorem3adant2 875 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
   =>   
 
Theorem3adant3 876 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
   =>   
 
Theorem3ad2ant1 877 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
   =>   
 
Theorem3ad2ant2 878 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
   =>   
 
Theorem3ad2ant3 879 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
   =>   
 
Theoremsimp1l 880 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp1r 881 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp2l 882 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp2r 883 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp3l 884 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp3r 885 Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
 
Theoremsimp11 886 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp12 887 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp13 888 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp21 889 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp22 890 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp23 891 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp31 892 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp32 893 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimp33 894 Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
 
Theoremsimpll1 895 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimpll2 896 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimpll3 897 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimplr1 898 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimplr2 899 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
 
Theoremsimplr3 900 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
    < 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-2000 21 2001-2099
  Copyright terms: Public domain < Previous  Next >