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	3expib 1201	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	3com12 1202	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ph /\ ch ) -> th )
Theorem	3com13 1203	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3com23 1204	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3coml 1205	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3comr 1206	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ph /\ ps ) -> th )
Theorem	3adant3r1 1207	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adant3r2 1208	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adant3r3 1209	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	ad4ant123 1210	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> th )
Theorem	ad4ant124 1211	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ph /\ ps ) /\ ta ) /\ ch ) -> th )
Theorem	ad4ant134 1212	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) -> th )
Theorem	ad4ant234 1213	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ta /\ ph ) /\ ps ) /\ ch ) -> th )
Theorem	3an1rs 1214	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps /\ th ) /\ ch ) -> ta )
Theorem	3imp1 1215	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
Theorem	3impd 1216	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
Theorem	3imp2 1217	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
Theorem	3exp1 1218	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3expd 1219	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3exp2 1220	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp5o 1221	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 1222	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 1223	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 1224	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 1225	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph ) /\ ps /\ ch ) -> th )
Theorem	3adant1r 1226	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )
Theorem	3adant2l 1227	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th )
Theorem	3adant2r 1228	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th )
Theorem	3adant3l 1229	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th )
Theorem	3adant3r 1230	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )
Theorem	syl12anc 1231	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 1232	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 1233	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ph -> ta )
Theorem	syl22anc 1234	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 1235	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 1236	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 1237	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 1238	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 1239	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 1240	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 1241	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 1242	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 1243	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 1244	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 1245	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 1246	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 1247	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 1248	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 1249	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 1250	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 1251	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 1252	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 1253	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 1254	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 1255	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 1256	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 1257	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 1258	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 1259	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 1260	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 1261	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 1262	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 1263	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 1264	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 1265	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 1266	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2 1267	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3 1268	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1b 1269	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2b 1270	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3b 1271	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1br 1272	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ps <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2br 1273	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ch <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3br 1274	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( th <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an 1275	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 1276	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 1277	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 1278	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ta )
Theorem	syld3an1 1279	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|- ( ( ch /\ ps /\ th ) -> ph )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ch /\ ps /\ th ) -> ta )
Theorem	syld3an2 1280	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ch /\ th ) -> ps )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3anl1 1281	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ph /\ ch /\ th ) /\ ta ) -> et )
Theorem	syl3anl2 1282	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ph /\ th ) /\ ta ) -> et )
Theorem	syl3anl3 1283	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> th )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ch /\ ph ) /\ ta ) -> et )
Theorem	syl3anl 1284	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 1285	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|- ( ph -> ps )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ph /\ th /\ ta ) ) -> et )
Theorem	syl3anr2 1286	A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|- ( ph -> th )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ ph /\ ta ) ) -> et )
Theorem	syl3anr3 1287	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|- ( ph -> ta )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ th /\ ph ) ) -> et )
Theorem	3impdi 1288	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impdir 1289	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ ps ) ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3anidm12 1290	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm13 1291	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ps /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm23 1292	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
|- ( ( ph /\ ps /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	syl2an3an 1293	syl3an 1275 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 1294	Deduction related to syl3an 1275 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 1295	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
|- ( ph \/ ps \/ ch )   =>    |- ( ( -. ph /\ -. ps ) -> ch )
Theorem	3jao 1296	Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
Theorem	3jaob 1297	Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|- ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )
Theorem	3jaoi 1298	Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
|- ( ph -> ps )   &    |- ( ch -> ps )   &    |- ( th -> ps )   =>    |- ( ( ph \/ ch \/ th ) -> ps )
Theorem	3jaod 1299	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 1300	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 )