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.)
⊢ ((η ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ)) ∧ ζ) → χ)
Theorem	simp311 1102	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → φ)
Theorem	simp312 1103	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → ψ)
Theorem	simp313 1104	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ ((φ ∧ ψ ∧ χ) ∧ θ ∧ τ)) → χ)
Theorem	simp321 1105	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → φ)
Theorem	simp322 1106	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → ψ)
Theorem	simp323 1107	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ (φ ∧ ψ ∧ χ) ∧ τ)) → χ)
Theorem	simp331 1108	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → φ)
Theorem	simp332 1109	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → ψ)
Theorem	simp333 1110	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((η ∧ ζ ∧ (θ ∧ τ ∧ (φ ∧ ψ ∧ χ))) → χ)
Theorem	3adantl1 1111	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((τ ∧ φ ∧ ψ) ∧ χ) → θ)
Theorem	3adantl2 1112	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ τ ∧ ψ) ∧ χ) → θ)
Theorem	3adantl3 1113	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ ψ ∧ τ) ∧ χ) → θ)
Theorem	3adantr1 1114	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (τ ∧ ψ ∧ χ)) → θ)
Theorem	3adantr2 1115	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ τ ∧ χ)) → θ)
Theorem	3adantr3 1116	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ ∧ τ)) → θ)
Theorem	3ad2antl1 1117	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ ψ ∧ τ) ∧ χ) → θ)
Theorem	3ad2antl2 1118	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ (((ψ ∧ φ ∧ τ) ∧ χ) → θ)
Theorem	3ad2antl3 1119	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ (((ψ ∧ τ ∧ φ) ∧ χ) → θ)
Theorem	3ad2antr1 1120	Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (χ ∧ ψ ∧ τ)) → θ)
Theorem	3ad2antr2 1121	Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ ∧ τ)) → θ)
Theorem	3ad2antr3 1122	Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
⊢ ((φ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ τ ∧ χ)) → θ)
Theorem	3anibar 1123	Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)
⊢ ((φ ∧ ψ ∧ χ) → (θ ↔ (χ ∧ τ)))    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → (θ ↔ τ))
Theorem	3mix1 1124	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (φ → (φ ∨ ψ ∨ χ))
Theorem	3mix2 1125	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (φ → (ψ ∨ φ ∨ χ))
Theorem	3mix3 1126	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (φ → (ψ ∨ χ ∨ φ))
Theorem	3mix1i 1127	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ φ    ⇒   ⊢ (φ ∨ ψ ∨ χ)
Theorem	3mix2i 1128	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ φ    ⇒   ⊢ (ψ ∨ φ ∨ χ)
Theorem	3mix3i 1129	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ φ    ⇒   ⊢ (ψ ∨ χ ∨ φ)
Theorem	3pm3.2i 1130	Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
⊢ φ    &   ⊢ ψ    &   ⊢ χ    ⇒   ⊢ (φ ∧ ψ ∧ χ)
Theorem	pm3.2an3 1131	pm3.2 434 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)
⊢ (φ → (ψ → (χ → (φ ∧ ψ ∧ χ))))
Theorem	3jca 1132	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    ⇒   ⊢ (φ → (ψ ∧ χ ∧ θ))
Theorem	3jcad 1133	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ → θ))    &   ⊢ (φ → (ψ → τ))    ⇒   ⊢ (φ → (ψ → (χ ∧ θ ∧ τ)))
Theorem	mpbir3an 1134	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)
⊢ ψ    &   ⊢ χ    &   ⊢ θ    &   ⊢ (φ ↔ (ψ ∧ χ ∧ θ))    ⇒   ⊢ φ
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.)
⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → (ψ ↔ (χ ∧ θ ∧ τ)))    ⇒   ⊢ (φ → ψ)
Theorem	syl3anbrc 1136	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (τ ↔ (ψ ∧ χ ∧ θ))    ⇒   ⊢ (φ → τ)
Theorem	3anim123i 1137	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ (φ → ψ)    &   ⊢ (χ → θ)    &   ⊢ (τ → η)    ⇒   ⊢ ((φ ∧ χ ∧ τ) → (ψ ∧ θ ∧ η))
Theorem	3anim1i 1138	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
⊢ (φ → ψ)    ⇒   ⊢ ((φ ∧ χ ∧ θ) → (ψ ∧ χ ∧ θ))
Theorem	3anim3i 1139	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (φ → ψ)    ⇒   ⊢ ((χ ∧ θ ∧ φ) → (χ ∧ θ ∧ ψ))
Theorem	3anbi123i 1140	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    &   ⊢ (τ ↔ η)    ⇒   ⊢ ((φ ∧ χ ∧ τ) ↔ (ψ ∧ θ ∧ η))
Theorem	3orbi123i 1141	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
⊢ (φ ↔ ψ)    &   ⊢ (χ ↔ θ)    &   ⊢ (τ ↔ η)    ⇒   ⊢ ((φ ∨ χ ∨ τ) ↔ (ψ ∨ θ ∨ η))
Theorem	3anbi1i 1142	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((φ ∧ χ ∧ θ) ↔ (ψ ∧ χ ∧ θ))
Theorem	3anbi2i 1143	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((χ ∧ φ ∧ θ) ↔ (χ ∧ ψ ∧ θ))
Theorem	3anbi3i 1144	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (φ ↔ ψ)    ⇒   ⊢ ((χ ∧ θ ∧ φ) ↔ (χ ∧ θ ∧ ψ))
Theorem	3imp 1145	Importation inference. (Contributed by NM, 8-Apr-1994.)
⊢ (φ → (ψ → (χ → θ)))    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impa 1146	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impb 1147	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impia 1148	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ ((φ ∧ ψ) → (χ → θ))    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3impib 1149	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ (φ → ((ψ ∧ χ) → θ))    ⇒   ⊢ ((φ ∧ ψ ∧ χ) → θ)
Theorem	3exp 1150	Exportation inference. (Contributed by NM, 30-May-1994.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (φ → (ψ → (χ → θ)))
Theorem	3expa 1151	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ ψ) ∧ χ) → θ)
Theorem	3expb 1152	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)
Theorem	3expia 1153	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ) → (χ → θ))
Theorem	3expib 1154	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (φ → ((ψ ∧ χ) → θ))
Theorem	3com12 1155	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ φ ∧ χ) → θ)
Theorem	3com13 1156	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((χ ∧ ψ ∧ φ) → θ)
Theorem	3com23 1157	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ χ ∧ ψ) → θ)
Theorem	3coml 1158	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((ψ ∧ χ ∧ φ) → θ)
Theorem	3comr 1159	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((χ ∧ φ ∧ ψ) → θ)
Theorem	3adant3r1 1160	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (τ ∧ ψ ∧ χ)) → θ)
Theorem	3adant3r2 1161	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ τ ∧ χ)) → θ)
Theorem	3adant3r3 1162	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ χ ∧ τ)) → θ)
Theorem	3an1rs 1163	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (((φ ∧ ψ ∧ θ) ∧ χ) → τ)
Theorem	3imp1 1164	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → τ)
Theorem	3impd 1165	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ (φ → ((ψ ∧ χ ∧ θ) → τ))
Theorem	3imp2 1166	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (φ → (ψ → (χ → (θ → τ))))    ⇒   ⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → τ)
Theorem	3exp1 1167	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (((φ ∧ ψ ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	3expd 1168	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (φ → ((ψ ∧ χ ∧ θ) → τ))    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	3exp2 1169	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → τ)    ⇒   ⊢ (φ → (ψ → (χ → (θ → τ))))
Theorem	exp5o 1170	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ ((φ ∧ ψ ∧ χ) → ((θ ∧ τ) → η))    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp516 1171	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((φ ∧ (ψ ∧ χ ∧ θ)) ∧ τ) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	exp520 1172	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((φ ∧ ψ ∧ χ) ∧ (θ ∧ τ)) → η)    ⇒   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
Theorem	3anassrs 1173	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((φ ∧ (ψ ∧ χ ∧ θ)) → τ)    ⇒   ⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ) → τ)
Theorem	3adant1l 1174	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (((τ ∧ φ) ∧ ψ ∧ χ) → θ)
Theorem	3adant1r 1175	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ τ) ∧ ψ ∧ χ) → θ)
Theorem	3adant2l 1176	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (τ ∧ ψ) ∧ χ) → θ)
Theorem	3adant2r 1177	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ τ) ∧ χ) → θ)
Theorem	3adant3l 1178	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ (τ ∧ χ)) → θ)
Theorem	3adant3r 1179	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ ∧ χ) → θ)    ⇒   ⊢ ((φ ∧ ψ ∧ (χ ∧ τ)) → θ)
Theorem	syl12anc 1180	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ ((ψ ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ (φ → τ)
Theorem	syl21anc 1181	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (((ψ ∧ χ) ∧ θ) → τ)    ⇒   ⊢ (φ → τ)
Theorem	syl3anc 1182	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ ((ψ ∧ χ ∧ θ) → τ)    ⇒   ⊢ (φ → τ)
Theorem	syl22anc 1183	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ)) → η)    ⇒   ⊢ (φ → η)
Theorem	syl13anc 1184	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ ((ψ ∧ (χ ∧ θ ∧ τ)) → η)    ⇒   ⊢ (φ → η)
Theorem	syl31anc 1185	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (((ψ ∧ χ ∧ θ) ∧ τ) → η)    ⇒   ⊢ (φ → η)
Theorem	syl112anc 1186	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ ((ψ ∧ χ ∧ (θ ∧ τ)) → η)    ⇒   ⊢ (φ → η)
Theorem	syl121anc 1187	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ ((ψ ∧ (χ ∧ θ) ∧ τ) → η)    ⇒   ⊢ (φ → η)
Theorem	syl211anc 1188	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (((ψ ∧ χ) ∧ θ ∧ τ) → η)    ⇒   ⊢ (φ → η)
Theorem	syl23anc 1189	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ ∧ η)) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl32anc 1190	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (((ψ ∧ χ ∧ θ) ∧ (τ ∧ η)) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl122anc 1191	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ ((ψ ∧ (χ ∧ θ) ∧ (τ ∧ η)) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl212anc 1192	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (((ψ ∧ χ) ∧ θ ∧ (τ ∧ η)) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl221anc 1193	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ) ∧ η) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl113anc 1194	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ ((ψ ∧ χ ∧ (θ ∧ τ ∧ η)) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl131anc 1195	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ ((ψ ∧ (χ ∧ θ ∧ τ) ∧ η) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl311anc 1196	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (((ψ ∧ χ ∧ θ) ∧ τ ∧ η) → ζ)    ⇒   ⊢ (φ → ζ)
Theorem	syl33anc 1197	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (φ → ζ)    &   ⊢ (((ψ ∧ χ ∧ θ) ∧ (τ ∧ η ∧ ζ)) → σ)    ⇒   ⊢ (φ → σ)
Theorem	syl222anc 1198	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (φ → ζ)    &   ⊢ (((ψ ∧ χ) ∧ (θ ∧ τ) ∧ (η ∧ ζ)) → σ)    ⇒   ⊢ (φ → σ)
Theorem	syl123anc 1199	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (φ → ζ)    &   ⊢ ((ψ ∧ (χ ∧ θ) ∧ (τ ∧ η ∧ ζ)) → σ)    ⇒   ⊢ (φ → σ)
Theorem	syl132anc 1200	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    &   ⊢ (φ → θ)    &   ⊢ (φ → τ)    &   ⊢ (φ → η)    &   ⊢ (φ → ζ)    &   ⊢ ((ψ ∧ (χ ∧ θ ∧ τ) ∧ (η ∧ ζ)) → σ)    ⇒   ⊢ (φ → σ)