P. 12 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 1101-1200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simp231 1101	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ph )
Theorem	simp232 1102	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ps )
Theorem	simp233 1103	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ch )
Theorem	simp311 1104	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ph )
Theorem	simp312 1105	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )
Theorem	simp313 1106	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ch )
Theorem	simp321 1107	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ph )
Theorem	simp322 1108	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ps )
Theorem	simp323 1109	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ch )
Theorem	simp331 1110	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp332 1111	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp333 1112	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	3adantl1 1113	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph /\ ps ) /\ ch ) -> th )
Theorem	3adantl2 1114	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta /\ ps ) /\ ch ) -> th )
Theorem	3adantl3 1115	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3adantr1 1116	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adantr2 1117	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adantr3 1118	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antl1 1119	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl2 1120	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl3 1121	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ta /\ ph ) /\ ch ) -> th )
Theorem	3ad2antr1 1122	Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )
Theorem	3ad2antr2 1123	Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antr3 1124	Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3anibar 1125	Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)
|- ( ( ph /\ ps /\ ch ) -> ( th <-> ( ch /\ ta ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )
Theorem	3mix1 1126	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ph \/ ps \/ ch ) )
Theorem	3mix2 1127	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ps \/ ph \/ ch ) )
Theorem	3mix3 1128	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ps \/ ch \/ ph ) )
Theorem	3mix1i 1129	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ph \/ ps \/ ch )
Theorem	3mix2i 1130	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ps \/ ph \/ ch )
Theorem	3mix3i 1131	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ps \/ ch \/ ph )
Theorem	3pm3.2i 1132	Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|- ph   &    |- ps   &    |- ch   =>    |- ( ph /\ ps /\ ch )
Theorem	pm3.2an3 1133	pm3.2 435 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
Theorem	3jca 1134	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps /\ ch /\ th ) )
Theorem	3jcad 1135	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 1136	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)
|- ps   &    |- ch   &    |- th   &    |- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ph
Theorem	mpbir3and 1137	Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)
|- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )   =>    |- ( ph -> ps )
Theorem	syl3anbrc 1138	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ta <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ta )
Theorem	3anim123i 1139	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 1140	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
Theorem	3anim3i 1141	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ch /\ th /\ ph ) -> ( ch /\ th /\ ps ) )
Theorem	3anbi123i 1142	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 1143	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 1144	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 1145	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 1146	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 1147	Importation inference. (Contributed by NM, 8-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impa 1148	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impb 1149	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impia 1150	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ( ph /\ ps ) -> ( ch -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impib 1151	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|- ( ph -> ( ( ps /\ ch ) -> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3exp 1152	Exportation inference. (Contributed by NM, 30-May-1994.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	3expa 1153	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps ) /\ ch ) -> th )
Theorem	3expb 1154	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> th )
Theorem	3expia 1155	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> ( ch -> th ) )
Theorem	3expib 1156	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> ( ( ps /\ ch ) -> th ) )
Theorem	3com12 1157	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 1158	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3com23 1159	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3coml 1160	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3comr 1161	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ch /\ ph /\ ps ) -> th )
Theorem	3adant3r1 1162	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adant3r2 1163	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adant3r3 1164	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3an1rs 1165	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps /\ th ) /\ ch ) -> ta )
Theorem	3imp1 1166	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
Theorem	3impd 1167	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )
Theorem	3imp2 1168	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )   =>    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
Theorem	3exp1 1169	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3expd 1170	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	3exp2 1171	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
Theorem	exp5o 1172	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 1173	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 1174	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 1175	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 1176	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph ) /\ ps /\ ch ) -> th )
Theorem	3adant1r 1177	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta ) /\ ps /\ ch ) -> th )
Theorem	3adant2l 1178	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th )
Theorem	3adant2r 1179	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th )
Theorem	3adant3l 1180	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th )
Theorem	3adant3r 1181	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th )
Theorem	syl12anc 1182	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 1183	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 1184	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ph -> ta )
Theorem	syl22anc 1185	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 1186	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 1187	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 1188	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 1189	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 1190	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 1191	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 1192	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 1193	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 1194	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 1195	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 1196	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 1197	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 1198	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 1199	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 1200	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 )