Type  Label  Description 
Statement 

Theorem  simp233 1101 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp311 1102 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp312 1103 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp313 1104 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp321 1105 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp322 1106 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp323 1107 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp331 1108 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp332 1109 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  simp333 1110 
Simplification of conjunction. (Contributed by NM, 9Mar2012.)



Theorem  3adantl1 1111 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantl2 1112 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantl3 1113 
Deduction adding a conjunct to antecedent. (Contributed by NM,
24Feb2005.)



Theorem  3adantr1 1114 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3adantr2 1115 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3adantr3 1116 
Deduction adding a conjunct to antecedent. (Contributed by NM,
27Apr2005.)



Theorem  3ad2antl1 1117 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antl2 1118 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antl3 1119 
Deduction adding conjuncts to antecedent. (Contributed by NM,
4Aug2007.)



Theorem  3ad2antr1 1120 
Deduction adding conjuncts to antecedent. (Contributed by NM,
25Dec2007.)



Theorem  3ad2antr2 1121 
Deduction adding conjuncts to antecedent. (Contributed by NM,
27Dec2007.)



Theorem  3ad2antr3 1122 
Deduction adding conjuncts to antecedent. (Contributed by NM,
30Dec2007.)



Theorem  3anibar 1123 
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22Jul2008.)



Theorem  3mix1 1124 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix2 1125 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix3 1126 
Introduction in triple disjunction. (Contributed by NM, 4Apr1995.)



Theorem  3mix1i 1127 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3mix2i 1128 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3mix3i 1129 
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6Oct2014.)



Theorem  3pm3.2i 1130 
Infer conjunction of premises. (Contributed by NM, 10Feb1995.)



Theorem  pm3.2an3 1131 
pm3.2 434 for a triple conjunction. (Contributed by
Alan Sare,
24Oct2011.)



Theorem  3jca 1132 
Join consequents with conjunction. (Contributed by NM, 9Apr1994.)



Theorem  3jcad 1133 
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25Sep2005.)



Theorem  mpbir3an 1134 
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16Sep2011.)



Theorem  mpbir3and 1135 
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11May2014.) (Revised by Mario Carneiro,
9Jan2015.)



Theorem  syl3anbrc 1136 
Syllogism inference. (Contributed by Mario Carneiro, 11May2014.)



Theorem  3anim123i 1137 
Join antecedents and consequents with conjunction. (Contributed by NM,
8Apr1994.)



Theorem  3anim1i 1138 
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16Aug2009.)



Theorem  3anim3i 1139 
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19Aug2009.)



Theorem  3anbi123i 1140 
Join 3 biconditionals with conjunction. (Contributed by NM,
21Apr1994.)



Theorem  3orbi123i 1141 
Join 3 biconditionals with disjunction. (Contributed by NM,
17May1994.)



Theorem  3anbi1i 1142 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3anbi2i 1143 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3anbi3i 1144 
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8Sep2006.)



Theorem  3imp 1145 
Importation inference. (Contributed by NM, 8Apr1994.)



Theorem  3impa 1146 
Importation from double to triple conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3impb 1147 
Importation from double to triple conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3impia 1148 
Importation to triple conjunction. (Contributed by NM, 13Jun2006.)



Theorem  3impib 1149 
Importation to triple conjunction. (Contributed by NM, 13Jun2006.)



Theorem  3exp 1150 
Exportation inference. (Contributed by NM, 30May1994.)



Theorem  3expa 1151 
Exportation from triple to double conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3expb 1152 
Exportation from triple to double conjunction. (Contributed by NM,
20Aug1995.)



Theorem  3expia 1153 
Exportation from triple conjunction. (Contributed by NM,
19May2007.)



Theorem  3expib 1154 
Exportation from triple conjunction. (Contributed by NM,
19May2007.)



Theorem  3com12 1155 
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28Jan1996.) (Proof shortened by Andrew Salmon, 13May2011.)



Theorem  3com13 1156 
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28Jan1996.)



Theorem  3com23 1157 
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28Jan1996.)



Theorem  3coml 1158 
Commutation in antecedent. Rotate left. (Contributed by NM,
28Jan1996.)



Theorem  3comr 1159 
Commutation in antecedent. Rotate right. (Contributed by NM,
28Jan1996.)



Theorem  3adant3r1 1160 
Deduction adding a conjunct to antecedent. (Contributed by NM,
16Feb2008.)



Theorem  3adant3r2 1161 
Deduction adding a conjunct to antecedent. (Contributed by NM,
17Feb2008.)



Theorem  3adant3r3 1162 
Deduction adding a conjunct to antecedent. (Contributed by NM,
18Feb2008.)



Theorem  3an1rs 1163 
Swap conjuncts. (Contributed by NM, 16Dec2007.)



Theorem  3imp1 1164 
Importation to left triple conjunction. (Contributed by NM,
24Feb2005.)



Theorem  3impd 1165 
Importation deduction for triple conjunction. (Contributed by NM,
26Oct2006.)



Theorem  3imp2 1166 
Importation to right triple conjunction. (Contributed by NM,
26Oct2006.)



Theorem  3exp1 1167 
Exportation from left triple conjunction. (Contributed by NM,
24Feb2005.)



Theorem  3expd 1168 
Exportation deduction for triple conjunction. (Contributed by NM,
26Oct2006.)



Theorem  3exp2 1169 
Exportation from right triple conjunction. (Contributed by NM,
26Oct2006.)



Theorem  exp5o 1170 
A triple exportation inference. (Contributed by Jeff Hankins,
8Jul2009.)



Theorem  exp516 1171 
A triple exportation inference. (Contributed by Jeff Hankins,
8Jul2009.)



Theorem  exp520 1172 
A triple exportation inference. (Contributed by Jeff Hankins,
8Jul2009.)



Theorem  3anassrs 1173 
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4Jan2017.)



Theorem  3adant1l 1174 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  3adant1r 1175 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  3adant2l 1176 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  3adant2r 1177 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  3adant3l 1178 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  3adant3r 1179 
Deduction adding a conjunct to antecedent. (Contributed by NM,
8Jan2006.)



Theorem  syl12anc 1180 
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1Aug2009.)



Theorem  syl21anc 1181 
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1Aug2009.)



Theorem  syl3anc 1182 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl22anc 1183 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl13anc 1184 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl31anc 1185 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl112anc 1186 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl121anc 1187 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl211anc 1188 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl23anc 1189 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl32anc 1190 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl122anc 1191 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl212anc 1192 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl221anc 1193 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl113anc 1194 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl131anc 1195 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl311anc 1196 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl33anc 1197 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl222anc 1198 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl123anc 1199 
Syllogism combined with contraction. (Contributed by NM,
11Mar2012.)



Theorem  syl132anc 1200 
Syllogism combined with contraction. (Contributed by NM,
11Jul2012.)

