P. 15 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1401-1500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	syl131anc 1401	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl311anc 1402	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl33anc 1403	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl222anc 1404	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl123anc 1405	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl132anc 1406	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl213anc 1407	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl231anc 1408	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl312anc 1409	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl321anc 1410	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl133anc 1411	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl313anc 1412	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl331anc 1413	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl223anc 1414	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl232anc 1415	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl322anc 1416	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl233anc 1417	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl323anc 1418	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl332anc 1419	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl333anc 1420	A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (𝜑 → 𝜇)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)    ⇒   ⊢ (𝜑 → 𝜆)
Theorem	syl3an1b 1421	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2b 1422	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3b 1423	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1br 1424	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2br 1425	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3br 1426	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜃 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syld3an3 1427	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
Theorem	syld3an1 1428	A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)
Theorem	syld3an2 1429	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3anl1 1430	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl2 1431	A syllogism inference. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl3 1432	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂)
Theorem	syl3anl 1433	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎)
Theorem	syl3anr1 1434	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr2 1435	A syllogism inference. (Contributed by NM, 1-Aug-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr3 1436	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂)
Theorem	3anidm12 1437	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm13 1438	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm23 1439	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	syl2an3an 1440	syl3an 1172 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜂)
Theorem	syl2an23an 1441	Deduction related to syl3an 1172 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜑) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜑) → 𝜂)
Theorem	3ori 1442	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)    ⇒   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	3jao 1443	Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
Theorem	3jaob 1444	Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaobOLD 1445	Obsolete version of 3jaob 1444 as of 29-Jun-2025. (Contributed by NM, 13-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaoi 1446	Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) (Proof shortened by Garrett Katz, 16-Jun-2026.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)
Theorem	3jaoiOLD 1447	Obsolete version of 3jaoi 1446 as of 16-Jun-2026. Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)
Theorem	3jaod 1448	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
Theorem	3jaoian 1449	Disjunction of three antecedents (inference). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜏 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	3jaodan 1450	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
Theorem	mpjao3dan 1451	Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	3jaao 1452	Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Garrett Katz, 16-Jun-2026.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    &   ⊢ (𝜂 → (𝜁 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → ((𝜓 ∨ 𝜏 ∨ 𝜁) → 𝜒))
Theorem	3jaaoOLD 1453	Obsolete version of 3jaao 1452 as of 16-Jun-2026. Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    &   ⊢ (𝜂 → (𝜁 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → ((𝜓 ∨ 𝜏 ∨ 𝜁) → 𝜒))
Theorem	syl3an9b 1454	Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    &   ⊢ (𝜂 → (𝜏 ↔ 𝜁))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁))
Theorem	3orbi123d 1455	Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	3anbi123d 1456	Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3anbi12d 1457	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))
Theorem	3anbi13d 1458	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))
Theorem	3anbi23d 1459	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi1d 1460	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	3anbi2d 1461	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi3d 1462	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))
Theorem	3anim123d 1463	Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3orim123d 1464	Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	an6 1465	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)))
Theorem	3an6 1466	Analogue of an4 666 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ (𝜓 ∧ 𝜃 ∧ 𝜂)))
Theorem	3or6 1467	Analogue of or4 937 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃) ∨ (𝜏 ∨ 𝜂)) ↔ ((𝜑 ∨ 𝜒 ∨ 𝜏) ∨ (𝜓 ∨ 𝜃 ∨ 𝜂)))
Theorem	mp3an1 1468	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mp3an2 1469	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mp3an3 1470	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mp3an12 1471	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mp3an13 1472	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	mp3an23 1473	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3an1i 1474	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	mp3anl1 1475	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl2 1476	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl3 1477	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜒    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
Theorem	mp3anr1 1478	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr2 1479	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr3 1480	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
⊢ 𝜃    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)
Theorem	mp3an 1481	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	mpd3an3 1482	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpd3an23 1483	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3and 1484	A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	mp3an12i 1485	mp3an 1481 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	mp3an2i 1486	mp3an 1481 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	mp3an3an 1487	mp3an 1481 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	mp3an2ani 1488	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	biimp3a 1489	Infer implication from a logical equivalence. Similar to biimpa 480. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	biimp3ar 1490	Infer implication from a logical equivalence. Similar to biimpar 481. (Contributed by NM, 2-Jan-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3anandis 1491	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3anandirs 1492	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ecase23d 1493	Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	3ecase 1494	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜃)    &   ⊢ (¬ 𝜓 → 𝜃)    &   ⊢ (¬ 𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	3bior1fd 1495	A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 947. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior1fand 1496	A disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ ((𝜃 ∧ 𝜏) ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior2fd 1497	A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 947. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3biant1d 1498	A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 539. (Contributed by Alexander van der Vekens, 26-Sep-2017.)
⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒 ∧ 𝜓)))
Theorem	intn3an1d 1499	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	intn3an2d 1500	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓 ∧ 𝜃))