Theorem List for Intuitionistic Logic Explorer - 1001-1100 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simp1r2 1001 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp1r3 1002 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l1 1003 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l2 1004 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2l3 1005 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r1 1006 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r2 1007 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp2r3 1008 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l1 1009 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l2 1010 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3l3 1011 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r1 1012 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r2 1013 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp3r3 1014 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp11l 1015 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp11r 1016 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp12l 1017 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp12r 1018 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp13l 1019 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp13r 1020 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp21l 1021 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp21r 1022 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp22l 1023 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp22r 1024 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23l 1025 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23r 1026 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31l 1027 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31r 1028 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32l 1029 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32r 1030 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33l 1031 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33r 1032 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp111 1033 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp112 1034 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp113 1035 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp121 1036 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp122 1037 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp123 1038 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp131 1039 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp132 1040 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp133 1041 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp211 1042 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp212 1043 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp213 1044 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp221 1045 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp222 1046 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp223 1047 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp231 1048 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp232 1049 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp233 1050 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp311 1051 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp312 1052 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp313 1053 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp321 1054 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp322 1055 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp323 1056 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp331 1057 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp332 1058 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp333 1059 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | 3adantl1 1060 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl2 1061 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl3 1062 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantr1 1063 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr2 1064 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr3 1065 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3ad2antl1 1066 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antl2 1067 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antl3 1068 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antr1 1069 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25-Dec-2007.)
|
|
|
Theorem | 3ad2antr2 1070 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27-Dec-2007.)
|
|
|
Theorem | 3ad2antr3 1071 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30-Dec-2007.)
|
|
|
Theorem | 3anibar 1072 |
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22-Jul-2008.)
|
|
|
Theorem | 3mix1 1073 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix2 1074 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix3 1075 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix1i 1076 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix2i 1077 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix3i 1078 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix1d 1079 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix2d 1080 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix3d 1081 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3pm3.2i 1082 |
Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | pm3.2an3 1083 |
pm3.2 126 for a triple conjunction. (Contributed by
Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | 3jca 1084 |
Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|
|
|
Theorem | 3jcad 1085 |
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25-Sep-2005.)
|
|
|
Theorem | mpbir3an 1086 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|
|
|
Theorem | mpbir3and 1087 |
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | syl3anbrc 1088 |
Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | 3anim123i 1089 |
Join antecedents and consequents with conjunction. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3anim1i 1090 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009.)
|
|
|
Theorem | 3anim2i 1091 |
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21-Nov-2019.)
|
|
|
Theorem | 3anim3i 1092 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19-Aug-2009.)
|
|
|
Theorem | 3anbi123i 1093 |
Join 3 biconditionals with conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3orbi123i 1094 |
Join 3 biconditionals with disjunction. (Contributed by NM,
17-May-1994.)
|
|
|
Theorem | 3anbi1i 1095 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi2i 1096 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi3i 1097 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3imp 1098 |
Importation inference. (Contributed by NM, 8-Apr-1994.)
|
|
|
Theorem | 3impa 1099 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3impb 1100 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|