Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simp22r 1101 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23l 1102 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp23r 1103 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31l 1104 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp31r 1105 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32l 1106 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp32r 1107 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33l 1108 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp33r 1109 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp111 1110 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp112 1111 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp113 1112 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp121 1113 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp122 1114 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp123 1115 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp131 1116 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp132 1117 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp133 1118 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp211 1119 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp212 1120 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp213 1121 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp221 1122 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp222 1123 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp223 1124 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp231 1125 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp232 1126 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp233 1127 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp311 1128 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp312 1129 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp313 1130 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp321 1131 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp322 1132 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp323 1133 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp331 1134 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp332 1135 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | simp333 1136 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
|
|
Theorem | 3adantl1 1137 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl2 1138 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantl3 1139 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3adantr1 1140 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr2 1141 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3adantr3 1142 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
|
|
Theorem | 3ad2antl1 1143 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antl2 1144 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antl3 1145 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antr1 1146 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25-Dec-2007.)
|
|
|
Theorem | 3ad2antr2 1147 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27-Dec-2007.)
|
|
|
Theorem | 3ad2antr3 1148 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30-Dec-2007.)
|
|
|
Theorem | 3anibar 1149 |
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22-Jul-2008.)
|
|
|
Theorem | 3mix1 1150 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix2 1151 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix3 1152 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix1i 1153 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix2i 1154 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix3i 1155 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix1d 1156 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix2d 1157 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix3d 1158 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3pm3.2i 1159 |
Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | pm3.2an3 1160 |
pm3.2 138 for a triple conjunction. (Contributed by
Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | 3jca 1161 |
Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|
|
|
Theorem | 3jcad 1162 |
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25-Sep-2005.)
|
|
|
Theorem | mpbir3an 1163 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|
|
|
Theorem | mpbir3and 1164 |
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | syl3anbrc 1165 |
Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | 3anim123i 1166 |
Join antecedents and consequents with conjunction. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3anim1i 1167 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009.)
|
|
|
Theorem | 3anim2i 1168 |
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21-Nov-2019.)
|
|
|
Theorem | 3anim3i 1169 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19-Aug-2009.)
|
|
|
Theorem | 3anbi123i 1170 |
Join 3 biconditionals with conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3orbi123i 1171 |
Join 3 biconditionals with disjunction. (Contributed by NM,
17-May-1994.)
|
|
|
Theorem | 3anbi1i 1172 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi2i 1173 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi3i 1174 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3imp 1175 |
Importation inference. (Contributed by NM, 8-Apr-1994.)
|
|
|
Theorem | 3impa 1176 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3impb 1177 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3impia 1178 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
|
|
Theorem | 3impib 1179 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
|
|
Theorem | 3exp 1180 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
|
|
Theorem | 3expa 1181 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3expb 1182 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3expia 1183 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
|
|
Theorem | 3expib 1184 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
|
|
Theorem | 3com12 1185 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
|
|
Theorem | 3com13 1186 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3com23 1187 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3coml 1188 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3comr 1189 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3adant3r1 1190 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
|
|
Theorem | 3adant3r2 1191 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
|
|
Theorem | 3adant3r3 1192 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
|
|
Theorem | ad4ant123 1193 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant124 1194 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant134 1195 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant234 1196 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | 3an1rs 1197 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
|
|
Theorem | 3imp1 1198 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3impd 1199 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3imp2 1200 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|