P. 12 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 1101-1200   *Has distinct variable group(s)

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