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	3impb 1201	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impia 1202	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impib 1203	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3exp 1204	Exportation inference. (Contributed by NM, 30-May-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	3expa 1205	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3expb 1206	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3expia 1207	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	3expib 1208	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	3com12 1209	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3com13 1210	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3com23 1211	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3coml 1212	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3comr 1213	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
Theorem	3adant3r1 1214	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r2 1215	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r3 1216	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad4ant123 1217	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)
Theorem	ad4ant124 1218	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	ad4ant134 1219	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad4ant234 1220	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3an1rs 1221	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏)
Theorem	3imp1 1222	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3impd 1223	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
Theorem	3imp2 1224	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3exp1 1225	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3expd 1226	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3exp2 1227	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5o 1228	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp516 1229	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp520 1230	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3anassrs 1231	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adant1l 1232	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant1r 1233	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant2l 1234	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant2r 1235	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adant3l 1236	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r 1237	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad5ant245 1238	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad5ant234 1239	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant235 1240	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant123 1241	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜃)
Theorem	ad5ant124 1242	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant125 1243	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant134 1244	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant135 1245	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant145 1246	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	syl12anc 1247	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 1248	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl3anc 1249	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 1250	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl13anc 1251	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl31anc 1252	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl112anc 1253	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl121anc 1254	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl211anc 1255	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl23anc 1256	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl32anc 1257	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl122anc 1258	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl212anc 1259	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl221anc 1260	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl113anc 1261	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl131anc 1262	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl311anc 1263	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl33anc 1264	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl222anc 1265	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl123anc 1266	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl132anc 1267	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl213anc 1268	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl231anc 1269	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl312anc 1270	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl321anc 1271	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl133anc 1272	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl313anc 1273	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl331anc 1274	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl223anc 1275	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl232anc 1276	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl322anc 1277	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl233anc 1278	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl323anc 1279	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl332anc 1280	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl333anc 1281	A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (𝜑 → 𝜇)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)    ⇒   ⊢ (𝜑 → 𝜆)
Theorem	syl3an1 1282	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2 1283	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3 1284	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1b 1285	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2b 1286	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3b 1287	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1br 1288	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2br 1289	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3br 1290	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜃 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an 1291	A triple syllogism inference. (Contributed by NM, 13-May-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anb 1292	A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anbr 1293	A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜒)    &   ⊢ (𝜂 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syld3an3 1294	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
Theorem	syld3an1 1295	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)
Theorem	syld3an2 1296	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3anl1 1297	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl2 1298	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl3 1299	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂)
Theorem	syl3anl 1300	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎)