P. 13 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1201-1300   *Has distinct variable group(s)

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