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	3jca 1201	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps /\ ch /\ th ) )
Theorem	3jcad 1202	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ps -> ta ) )   =>    |- ( ph -> ( ps -> ( ch /\ th /\ ta ) ) )
Theorem	mpbir3an 1203	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|- ps   &    |- ch   &    |- th   &    |- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ph
Theorem	mpbir3and 1204	Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
|- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )   =>    |- ( ph -> ps )
Theorem	syl3anbrc 1205	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ta <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ta )
Theorem	syl21anbrc 1206	Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ta <-> ( ( ps /\ ch ) /\ th ) )   =>    |- ( ph -> ta )
Theorem	3imp3i2an 1207	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ch ) -> ta )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ( ph /\ ps /\ ch ) -> et )
Theorem	3anim123i 1208	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ta -> et )   =>    |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )
Theorem	3anim1i 1209	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
Theorem	3anim2i 1210	Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ph /\ th ) -> ( ch /\ ps /\ th ) )
Theorem	3anim3i 1211	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ch /\ th /\ ph ) -> ( ch /\ th /\ ps ) )
Theorem	3anbi123i 1212	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- ( ( ph /\ ch /\ ta ) <-> ( ps /\ th /\ et ) )
Theorem	3orbi123i 1213	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) )
Theorem	3anbi1i 1214	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ph /\ ch /\ th ) <-> ( ps /\ ch /\ th ) )
Theorem	3anbi2i 1215	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ph /\ th ) <-> ( ch /\ ps /\ th ) )
Theorem	3anbi3i 1216	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ th /\ ph ) <-> ( ch /\ th /\ ps ) )
Theorem	3imp 1217	Importation inference. (Contributed by NM, 8-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impa 1218	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	ex3 1219	Apply ex 115 to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ( th -> ta ) )
Theorem	3imp31 1220	The importation inference 3imp 1217 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3imp231 1221	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3imp21 1222	The importation inference 3imp 1217 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1231 by Wolf Lammen, 23-Jun-2022.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ph /\ ch ) -> th )
Theorem	3impb 1223	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impia 1224	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impib 1225	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3exp 1226	Exportation inference. (Contributed by NM, 30-May-1994.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	3expa 1227	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	3expb 1228	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	3expia 1229	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	3expib 1230	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	3com12 1231	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 1232	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3com23 1233	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3coml 1234	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3comr 1235	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ph /\ ps ) -> th )
Theorem	3adant3r1 1236	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adant3r2 1237	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adant3r3 1238	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	ad4ant123 1239	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 1240	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 1241	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 1242	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 1243	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps /\ th ) /\ ch ) -> ta )
Theorem	3imp1 1244	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
Theorem	3impd 1245	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
Theorem	3imp2 1246	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
Theorem	3exp1 1247	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3expd 1248	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3exp2 1249	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp5o 1250	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 1251	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 1252	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 1253	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 1254	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph ) /\ ps /\ ch ) -> th )
Theorem	3adant1r 1255	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )
Theorem	3adant2l 1256	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th )
Theorem	3adant2r 1257	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th )
Theorem	3adant3l 1258	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th )
Theorem	3adant3r 1259	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )
Theorem	ad5ant245 1260	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 ) /\ et ) /\ ps ) /\ ch ) -> th )
Theorem	ad5ant234 1261	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 ) /\ et ) -> th )
Theorem	ad5ant235 1262	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 ) /\ et ) /\ ch ) -> th )
Theorem	ad5ant123 1263	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) /\ et ) -> th )
Theorem	ad5ant124 1264	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ps ) /\ ta ) /\ ch ) /\ et ) -> th )
Theorem	ad5ant125 1265	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ps ) /\ ta ) /\ et ) /\ ch ) -> th )
Theorem	ad5ant134 1266	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ta ) /\ ps ) /\ ch ) /\ et ) -> th )
Theorem	ad5ant135 1267	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ta ) /\ ps ) /\ et ) /\ ch ) -> th )
Theorem	ad5ant145 1268	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ( ( ph /\ ta ) /\ et ) /\ ps ) /\ ch ) -> th )
Theorem	syl12anc 1269	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 1270	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 1271	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ph -> ta )
Theorem	syl22anc 1272	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 1273	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 1274	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 1275	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 1276	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 1277	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 1278	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 1279	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 1280	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 1281	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 1282	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 1283	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 1284	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 1285	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 1286	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 1287	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 1288	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 1289	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 1290	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 1291	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 1292	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 1293	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 1294	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 1295	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 1296	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 1297	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 1298	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 1299	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 1300	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 )