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	3impia 1201	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impib 1202	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3exp 1203	Exportation inference. (Contributed by NM, 30-May-1994.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	3expa 1204	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	3expb 1205	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	3expia 1206	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	3expib 1207	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	3com12 1208	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 1209	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3com23 1210	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3coml 1211	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3comr 1212	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ph /\ ps ) -> th )
Theorem	3adant3r1 1213	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adant3r2 1214	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adant3r3 1215	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	ad4ant123 1216	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 1217	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 1218	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 1219	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 1220	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps /\ th ) /\ ch ) -> ta )
Theorem	3imp1 1221	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
Theorem	3impd 1222	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
Theorem	3imp2 1223	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
Theorem	3exp1 1224	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3expd 1225	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3exp2 1226	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp5o 1227	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 1228	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 1229	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 1230	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 1231	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph ) /\ ps /\ ch ) -> th )
Theorem	3adant1r 1232	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )
Theorem	3adant2l 1233	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th )
Theorem	3adant2r 1234	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th )
Theorem	3adant3l 1235	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th )
Theorem	3adant3r 1236	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )
Theorem	ad5ant245 1237	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 1238	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 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 )   =>    |- ( ( ( ( ( ta /\ ph ) /\ ps ) /\ et ) /\ ch ) -> th )
Theorem	ad5ant123 1240	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 1241	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 1242	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 1243	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 1244	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 1245	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 1246	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 1247	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 1248	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ph -> ta )
Theorem	syl22anc 1249	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 1250	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 1251	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 1252	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 1253	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 1254	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 1255	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 1256	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 1257	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 1258	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 1259	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 1260	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 1261	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 1262	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 1263	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 1264	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 1265	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 1266	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 1267	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 1268	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 1269	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 1270	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 1271	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 1272	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 1273	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 1274	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 1275	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 1276	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 1277	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 1278	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 1279	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 1280	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 1281	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2 1282	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3 1283	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1b 1284	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2b 1285	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3b 1286	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1br 1287	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ps <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2br 1288	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ch <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3br 1289	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( th <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an 1290	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 1291	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 1292	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 1293	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ta )
Theorem	syld3an1 1294	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|- ( ( ch /\ ps /\ th ) -> ph )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ch /\ ps /\ th ) -> ta )
Theorem	syld3an2 1295	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ch /\ th ) -> ps )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3anl1 1296	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ph /\ ch /\ th ) /\ ta ) -> et )
Theorem	syl3anl2 1297	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ph /\ th ) /\ ta ) -> et )
Theorem	syl3anl3 1298	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> th )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ch /\ ph ) /\ ta ) -> et )
Theorem	syl3anl 1299	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 1300	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|- ( ph -> ps )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ph /\ th /\ ta ) ) -> et )