Theorem List for Intuitionistic Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dn1dc 901 |
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 |
|
Theorem | pm5.71dc 902 |
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 |
|
Theorem | pm5.75 903 |
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.)
|
|
|
Theorem | bimsc1 904 |
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5-Aug-1993.)
|
|
|
Theorem | ccase 905 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
(Proof shortened by Wolf Lammen, 6-Jan-2013.)
|
|
|
Theorem | ccased 906 |
Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|
|
|
Theorem | ccase2 907 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|
|
|
Theorem | niabn 908 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
|
|
Theorem | dedlem0a 909 |
Alternate version of dedlema 910. (Contributed by NM, 2-Apr-1994.) (Proof
shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen,
4-Dec-2012.)
|
|
|
Theorem | dedlema 910 |
Lemma for iftrue 3356. (Contributed by NM, 26-Jun-2002.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
|
|
Theorem | dedlemb 911 |
Lemma for iffalse 3359. (Contributed by NM, 15-May-1999.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
|
|
Theorem | pm4.42r 912 |
One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed
by Jim Kingdon, 4-Aug-2018.)
|
|
|
Theorem | ninba 913 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
|
|
Theorem | prlem1 914 |
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.)
|
|
|
Theorem | prlem2 915 |
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.)
|
|
|
Theorem | oplem1 916 |
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.)
|
|
|
Theorem | rnlem 917 |
Lemma used in construction of real numbers. (Contributed by NM,
4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
|
|
1.2.12 Abbreviated conjunction and disjunction of
three wff's
|
|
Syntax | w3o 918 |
Extend wff definition to include 3-way disjunction ('or').
|
|
|
Syntax | w3a 919 |
Extend wff definition to include 3-way conjunction ('and').
|
|
|
Definition | df-3or 920 |
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 716. (Contributed by NM,
8-Apr-1994.)
|
|
|
Definition | df-3an 921 |
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 393. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3orass 922 |
Associative law for triple disjunction. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3anass 923 |
Associative law for triple conjunction. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3anrot 924 |
Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|
|
|
Theorem | 3orrot 925 |
Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3ancoma 926 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3ancomb 927 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3orcomb 928 |
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20-Apr-2011.)
|
|
|
Theorem | 3anrev 929 |
Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|
|
|
Theorem | 3anan32 930 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | 3anan12 931 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon,
14-Jun-2011.)
|
|
|
Theorem | anandi3 932 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
|
|
Theorem | anandi3r 933 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
|
|
Theorem | 3ioran 934 |
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19-Apr-2011.)
|
|
|
Theorem | 3simpa 935 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3simpb 936 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3simpc 937 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
|
|
Theorem | simp1 938 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simp2 939 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simp3 940 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | simpl1 941 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpl2 942 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpl3 943 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr1 944 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr2 945 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simpr3 946 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
|
|
Theorem | simp1i 947 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp2i 948 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp3i 949 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
|
|
Theorem | simp1d 950 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp2d 951 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp3d 952 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
|
|
Theorem | simp1bi 953 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | simp2bi 954 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | simp3bi 955 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | 3adant1 956 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3adant2 957 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3adant3 958 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
|
|
Theorem | 3ad2ant1 959 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | 3ad2ant2 960 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | 3ad2ant3 961 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
|
|
Theorem | simp1l 962 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp1r 963 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp2l 964 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp2r 965 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp3l 966 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp3r 967 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
|
|
Theorem | simp11 968 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp12 969 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp13 970 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp21 971 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp22 972 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp23 973 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp31 974 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp32 975 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simp33 976 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
|
|
Theorem | simpll1 977 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpll2 978 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpll3 979 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr1 980 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr2 981 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simplr3 982 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl1 983 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl2 984 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprl3 985 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr1 986 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr2 987 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simprr3 988 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl1l 989 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl1r 990 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl2l 991 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl2r 992 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl3l 993 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpl3r 994 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr1l 995 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr1r 996 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr2l 997 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr2r 998 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr3l 999 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simpr3r 1000 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|