Home Intuitionistic Logic ExplorerTheorem List (p. 11 of 22) < Previous  Next > Browser slow? Try the Unicode version.

Theorem List for Intuitionistic Logic Explorer - 1001-1100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremsimp223 1001 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp231 1002 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp232 1003 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp233 1004 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp311 1005 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp312 1006 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp313 1007 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp321 1008 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp322 1009 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp323 1010 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp331 1011 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp332 1012 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theoremsimp333 1013 Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Theorem3adantl1 1014 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Theorem3adantl2 1015 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Theorem3adantl3 1016 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)

Theorem3adantr1 1017 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Theorem3adantr2 1018 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Theorem3adantr3 1019 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)

Theorem3ad2antr1 1023 Deduction adding a conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)

Theorem3ad2antr2 1024 Deduction adding a conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)

Theorem3ad2antr3 1025 Deduction adding a conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)

Theorem3anibar 1026 Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)

Theorem3mix1 1027 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Theorem3mix2 1028 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Theorem3mix3 1029 Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)

Theorem3pm3.2i 1030 Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)

Theorempm3.2an3 1031 pm3.2 124 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)

Theorem3jca 1032 Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)

Theorem3jcad 1033 Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)

Theoremmpbir3an 1034 Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)

Theoremmpbir3and 1035 Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)

Theoremmpbir3anOLD 1036 Obsolete version of mpbir3an 1034 as of 9-Jan-2015. (Contributed by NM, 16-Sep-2011.)

Theoremmpbir3andOLD 1037 Obsolete version of mpbir3and 1035 as of 9-Jan-2015. (Contributed by NM, 11-May-2014.)

Theoremsyl3anbrc 1038 Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Theorem3anim123i 1039 Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)

Theorem3anim1i 1040 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)

Theorem3anim3i 1041 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)

Theorem3anbi123i 1042 Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)

Theorem3orbi123i 1043 Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)

Theorem3anbi1i 1044 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Theorem3anbi2i 1045 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Theorem3anbi3i 1046 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)

Theorem3imp 1047 Importation inference. (Contributed by NM, 8-Apr-1994.)

Theorem3impa 1048 Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Theorem3impb 1049 Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Theorem3impia 1050 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Theorem3impib 1051 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Theorem3exp 1052 Exportation inference. (Contributed by NM, 30-May-1994.)

Theorem3expa 1053 Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Theorem3expb 1054 Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Theorem3expia 1055 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Theorem3expib 1056 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Theorem3com12 1057 Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Theorem3com13 1058 Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)

Theorem3com23 1059 Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Theorem3coml 1060 Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)

Theorem3comr 1061 Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)

Theorem3adant3r1 1062 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)

Theorem3adant3r2 1063 Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)

Theorem3adant3r3 1064 Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)

Theorem3an1rs 1065 Swap conjuncts. (Contributed by NM, 16-Dec-2007.)

Theorem3imp1 1066 Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Theorem3impd 1067 Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Theorem3imp2 1068 Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Theorem3exp1 1069 Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)

Theorem3expd 1070 Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Theorem3exp2 1071 Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)

Theoremexp5o 1072 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)

Theoremexp516 1073 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)

Theoremexp520 1074 A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)

Theorem3adant1l 1075 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theorem3adant1r 1076 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theorem3adant2l 1077 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theorem3adant2r 1078 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theorem3adant3l 1079 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theorem3adant3r 1080 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Theoremsyl12anc 1081 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Theoremsyl21anc 1082 Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)

Theoremsyl3anc 1083 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl22anc 1084 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl13anc 1085 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl31anc 1086 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl112anc 1087 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl121anc 1088 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl211anc 1089 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl23anc 1090 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl32anc 1091 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl122anc 1092 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl212anc 1093 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl221anc 1094 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl113anc 1095 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl131anc 1096 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl311anc 1097 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl33anc 1098 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl222anc 1099 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Theoremsyl123anc 1100 Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

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-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-2186
 Copyright terms: Public domain < Previous  Next >