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	3comr 1201	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
Theorem	3adant3r1 1202	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r2 1203	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r3 1204	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad4ant123 1205	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)
Theorem	ad4ant124 1206	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	ad4ant134 1207	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad4ant234 1208	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3an1rs 1209	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏)
Theorem	3imp1 1210	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3impd 1211	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
Theorem	3imp2 1212	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3exp1 1213	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3expd 1214	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3exp2 1215	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5o 1216	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp516 1217	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp520 1218	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3anassrs 1219	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adant1l 1220	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant1r 1221	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant2l 1222	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant2r 1223	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adant3l 1224	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r 1225	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)
Theorem	syl12anc 1226	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 1227	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl3anc 1228	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 1229	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl13anc 1230	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl31anc 1231	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl112anc 1232	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl121anc 1233	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl211anc 1234	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl23anc 1235	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl32anc 1236	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl122anc 1237	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl212anc 1238	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl221anc 1239	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl113anc 1240	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl131anc 1241	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl311anc 1242	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl33anc 1243	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl222anc 1244	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl123anc 1245	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl132anc 1246	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl213anc 1247	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl231anc 1248	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl312anc 1249	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl321anc 1250	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl133anc 1251	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl313anc 1252	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl331anc 1253	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl223anc 1254	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl232anc 1255	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl322anc 1256	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl233anc 1257	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl323anc 1258	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl332anc 1259	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl333anc 1260	A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (𝜑 → 𝜇)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)    ⇒   ⊢ (𝜑 → 𝜆)
Theorem	syl3an1 1261	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2 1262	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3 1263	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1b 1264	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2b 1265	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3b 1266	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1br 1267	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2br 1268	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3br 1269	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜃 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an 1270	A triple syllogism inference. (Contributed by NM, 13-May-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anb 1271	A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anbr 1272	A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜒)    &   ⊢ (𝜂 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syld3an3 1273	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
Theorem	syld3an1 1274	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)
Theorem	syld3an2 1275	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3anl1 1276	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl2 1277	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl3 1278	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂)
Theorem	syl3anl 1279	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎)
Theorem	syl3anr1 1280	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr2 1281	A syllogism inference. (Contributed by NM, 1-Aug-2007.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr3 1282	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂)
Theorem	3impdi 1283	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impdir 1284	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3anidm12 1285	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm13 1286	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm23 1287	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	syl2an3an 1288	syl3an 1270 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜂)
Theorem	syl2an23an 1289	Deduction related to syl3an 1270 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜑) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜑) → 𝜂)
Theorem	3ori 1290	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)    ⇒   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	3jao 1291	Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
Theorem	3jaob 1292	Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaoi 1293	Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)
Theorem	3jaod 1294	Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
Theorem	3jaoian 1295	Disjunction of 3 antecedents (inference). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜏 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	3jaodan 1296	Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
Theorem	mpjao3dan 1297	Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	3jaao 1298	Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    &   ⊢ (𝜂 → (𝜁 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → ((𝜓 ∨ 𝜏 ∨ 𝜁) → 𝜒))
Theorem	3ianorr 1299	Triple disjunction implies negated triple conjunction. (Contributed by Jim Kingdon, 23-Dec-2018.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) → ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	syl3an9b 1300	Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    &   ⊢ (𝜂 → (𝜏 ↔ 𝜁))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁))