Theorem List for Intuitionistic Logic Explorer - 1201-1300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3adant3r1 1201 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
|
|
Theorem | 3adant3r2 1202 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
|
|
Theorem | 3adant3r3 1203 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
|
|
Theorem | ad4ant123 1204 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant124 1205 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant134 1206 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | ad4ant234 1207 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
|
|
Theorem | 3an1rs 1208 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
|
|
Theorem | 3imp1 1209 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3impd 1210 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3imp2 1211 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3exp1 1212 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3expd 1213 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3exp2 1214 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | exp5o 1215 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | exp516 1216 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | exp520 1217 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | 3anassrs 1218 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | 3adant1l 1219 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant1r 1220 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant2l 1221 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant2r 1222 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant3l 1223 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant3r 1224 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | syl12anc 1225 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
|
|
Theorem | syl21anc 1226 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
|
|
Theorem | syl3anc 1227 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl22anc 1228 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl13anc 1229 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl31anc 1230 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl112anc 1231 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl121anc 1232 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl211anc 1233 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl23anc 1234 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl32anc 1235 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl122anc 1236 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl212anc 1237 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl221anc 1238 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl113anc 1239 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl131anc 1240 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl311anc 1241 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl33anc 1242 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl222anc 1243 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl123anc 1244 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl132anc 1245 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl213anc 1246 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl231anc 1247 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl312anc 1248 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl321anc 1249 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl133anc 1250 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl313anc 1251 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl331anc 1252 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl223anc 1253 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl232anc 1254 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl322anc 1255 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl233anc 1256 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl323anc 1257 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl332anc 1258 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl333anc 1259 |
A syllogism inference combined with contraction. (Contributed by NM,
10-Mar-2012.)
|
|
|
Theorem | syl3an1 1260 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an2 1261 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an3 1262 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an1b 1263 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an2b 1264 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an3b 1265 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an1br 1266 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an2br 1267 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an3br 1268 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
|
|
Theorem | syl3an 1269 |
A triple syllogism inference. (Contributed by NM, 13-May-2004.)
|
|
|
Theorem | syl3anb 1270 |
A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
|
|
|
Theorem | syl3anbr 1271 |
A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
|
|
|
Theorem | syld3an3 1272 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
|
|
Theorem | syld3an1 1273 |
A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|
|
|
Theorem | syld3an2 1274 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
|
|
Theorem | syl3anl1 1275 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | syl3anl2 1276 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | syl3anl3 1277 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
|
|
Theorem | syl3anl 1278 |
A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
|
|
|
Theorem | syl3anr1 1279 |
A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|
|
|
Theorem | syl3anr2 1280 |
A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|
|
|
Theorem | syl3anr3 1281 |
A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|
|
|
Theorem | 3impdi 1282 |
Importation inference (undistribute conjunction). (Contributed by NM,
14-Aug-1995.)
|
|
|
Theorem | 3impdir 1283 |
Importation inference (undistribute conjunction). (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3anidm12 1284 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
|
|
Theorem | 3anidm13 1285 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
|
|
Theorem | 3anidm23 1286 |
Inference from idempotent law for conjunction. (Contributed by NM,
1-Feb-2007.)
|
|
|
Theorem | syl2an3an 1287 |
syl3an 1269 with antecedents in standard conjunction
form. (Contributed by
Alan Sare, 31-Aug-2016.)
|
|
|
Theorem | syl2an23an 1288 |
Deduction related to syl3an 1269 with antecedents in standard conjunction
form. (Contributed by Alan Sare, 31-Aug-2016.)
|
|
|
Theorem | 3ori 1289 |
Infer implication from triple disjunction. (Contributed by NM,
26-Sep-2006.)
|
|
|
Theorem | 3jao 1290 |
Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|
|
|
Theorem | 3jaob 1291 |
Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|
|
|
Theorem | 3jaoi 1292 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
12-Sep-1995.)
|
|
|
Theorem | 3jaod 1293 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | 3jaoian 1294 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | 3jaodan 1295 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
|
|
Theorem | mpjao3dan 1296 |
Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry
Arnoux, 13-Apr-2018.)
|
|
|
Theorem | 3jaao 1297 |
Inference conjoining and disjoining the antecedents of three
implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof
shortened by Andrew Salmon, 13-May-2011.)
|
|
|
Theorem | 3ianorr 1298 |
Triple disjunction implies negated triple conjunction. (Contributed by
Jim Kingdon, 23-Dec-2018.)
|
|
|
Theorem | syl3an9b 1299 |
Nested syllogism inference conjoining 3 dissimilar antecedents.
(Contributed by NM, 1-May-1995.)
|
|
|
Theorem | 3orbi123d 1300 |
Deduction joining 3 equivalences to form equivalence of disjunctions.
(Contributed by NM, 20-Apr-1994.)
|
|