Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3ad2antl2 1101 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antl3 1102 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
|
|
Theorem | 3ad2antr1 1103 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25-Dec-2007.)
|
|
|
Theorem | 3ad2antr2 1104 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27-Dec-2007.)
|
|
|
Theorem | 3ad2antr3 1105 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30-Dec-2007.)
|
|
|
Theorem | 3anibar 1106 |
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22-Jul-2008.)
|
|
|
Theorem | 3mix1 1107 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix2 1108 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix3 1109 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
|
|
Theorem | 3mix1i 1110 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix2i 1111 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix3i 1112 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
|
|
Theorem | 3mix1d 1113 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix2d 1114 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3mix3d 1115 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
|
|
Theorem | 3pm3.2i 1116 |
Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|
|
|
Theorem | pm3.2an3 1117 |
pm3.2 137 for a triple conjunction. (Contributed by
Alan Sare,
24-Oct-2011.)
|
|
|
Theorem | 3jca 1118 |
Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|
|
|
Theorem | 3jcad 1119 |
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25-Sep-2005.)
|
|
|
Theorem | mpbir3an 1120 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|
|
|
Theorem | mpbir3and 1121 |
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | syl3anbrc 1122 |
Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|
|
|
Theorem | 3anim123i 1123 |
Join antecedents and consequents with conjunction. (Contributed by NM,
8-Apr-1994.)
|
|
|
Theorem | 3anim1i 1124 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009.)
|
|
|
Theorem | 3anim2i 1125 |
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21-Nov-2019.)
|
|
|
Theorem | 3anim3i 1126 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19-Aug-2009.)
|
|
|
Theorem | 3anbi123i 1127 |
Join 3 biconditionals with conjunction. (Contributed by NM,
21-Apr-1994.)
|
|
|
Theorem | 3orbi123i 1128 |
Join 3 biconditionals with disjunction. (Contributed by NM,
17-May-1994.)
|
|
|
Theorem | 3anbi1i 1129 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi2i 1130 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3anbi3i 1131 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
|
|
Theorem | 3imp 1132 |
Importation inference. (Contributed by NM, 8-Apr-1994.)
|
|
|
Theorem | 3impa 1133 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3impb 1134 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3impia 1135 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
|
|
Theorem | 3impib 1136 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
|
|
Theorem | 3exp 1137 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
|
|
Theorem | 3expa 1138 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3expb 1139 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
|
|
Theorem | 3expia 1140 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
|
|
Theorem | 3expib 1141 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
|
|
Theorem | 3com12 1142 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
|
|
Theorem | 3com13 1143 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3com23 1144 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3coml 1145 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3comr 1146 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
|
|
Theorem | 3adant3r1 1147 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
|
|
Theorem | 3adant3r2 1148 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
|
|
Theorem | 3adant3r3 1149 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
|
|
Theorem | 3an1rs 1150 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
|
|
Theorem | 3imp1 1151 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3impd 1152 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3imp2 1153 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3exp1 1154 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
|
|
Theorem | 3expd 1155 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | 3exp2 1156 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
|
|
Theorem | exp5o 1157 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | exp516 1158 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | exp520 1159 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
|
|
Theorem | 3anassrs 1160 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | 3adant1l 1161 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant1r 1162 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant2l 1163 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant2r 1164 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant3l 1165 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | 3adant3r 1166 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
|
|
Theorem | syl12anc 1167 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
|
|
Theorem | syl21anc 1168 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
|
|
Theorem | syl3anc 1169 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl22anc 1170 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl13anc 1171 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl31anc 1172 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl112anc 1173 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl121anc 1174 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl211anc 1175 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl23anc 1176 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl32anc 1177 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl122anc 1178 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl212anc 1179 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl221anc 1180 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl113anc 1181 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl131anc 1182 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl311anc 1183 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl33anc 1184 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl222anc 1185 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl123anc 1186 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl132anc 1187 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl213anc 1188 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl231anc 1189 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl312anc 1190 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl321anc 1191 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
|
|
Theorem | syl133anc 1192 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl313anc 1193 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl331anc 1194 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl223anc 1195 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl232anc 1196 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl322anc 1197 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl233anc 1198 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl323anc 1199 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|
|
Theorem | syl332anc 1200 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
|