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	syl322anc 1401	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl233anc 1402	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl323anc 1403	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl332anc 1404	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)
Theorem	syl333anc 1405	A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (𝜑 → 𝜇)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆)    ⇒   ⊢ (𝜑 → 𝜆)
Theorem	syl3an1b 1406	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2b 1407	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3b 1408	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1br 1409	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2br 1410	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3br 1411	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜃 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syld3an3 1412	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
Theorem	syld3an1 1413	A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)
Theorem	syld3an2 1414	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3anl1 1415	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl2 1416	A syllogism inference. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl3 1417	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂)
Theorem	syl3anl 1418	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎)
Theorem	syl3anr1 1419	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr2 1420	A syllogism inference. (Contributed by NM, 1-Aug-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr3 1421	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂)
Theorem	3anidm12 1422	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm13 1423	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm23 1424	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	syl2an3an 1425	syl3an 1161 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜂)
Theorem	syl2an23an 1426	Deduction related to syl3an 1161 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜑) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜑) → 𝜂)
Theorem	3ori 1427	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)    ⇒   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	3jao 1428	Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
Theorem	3jaob 1429	Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.) (Proof shortened by Hongxiu Chen, 29-Jun-2025.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaobOLD 1430	Obsolete version of 3jaob 1429 as of 29-Jun-2025. (Contributed by NM, 13-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaoi 1431	Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)
Theorem	3jaod 1432	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
Theorem	3jaoian 1433	Disjunction of three antecedents (inference). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜏 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	3jaodan 1434	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
Theorem	mpjao3dan 1435	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 1436	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	syl3an9b 1437	Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    &   ⊢ (𝜂 → (𝜏 ↔ 𝜁))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁))
Theorem	3orbi123d 1438	Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	3anbi123d 1439	Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3anbi12d 1440	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))
Theorem	3anbi13d 1441	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))
Theorem	3anbi23d 1442	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi1d 1443	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	3anbi2d 1444	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi3d 1445	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))
Theorem	3anim123d 1446	Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3orim123d 1447	Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	an6 1448	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)))
Theorem	3an6 1449	Analogue of an4 657 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ (𝜓 ∧ 𝜃 ∧ 𝜂)))
Theorem	3or6 1450	Analogue of or4 927 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃) ∨ (𝜏 ∨ 𝜂)) ↔ ((𝜑 ∨ 𝜒 ∨ 𝜏) ∨ (𝜓 ∨ 𝜃 ∨ 𝜂)))
Theorem	mp3an1 1451	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mp3an2 1452	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mp3an3 1453	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mp3an12 1454	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mp3an13 1455	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	mp3an23 1456	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3an1i 1457	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	mp3anl1 1458	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl2 1459	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl3 1460	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜒    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
Theorem	mp3anr1 1461	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr2 1462	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr3 1463	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
⊢ 𝜃    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)
Theorem	mp3an 1464	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	mpd3an3 1465	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpd3an23 1466	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3and 1467	A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	mp3an12i 1468	mp3an 1464 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	mp3an2i 1469	mp3an 1464 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	mp3an3an 1470	mp3an 1464 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	mp3an2ani 1471	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	biimp3a 1472	Infer implication from a logical equivalence. Similar to biimpa 476. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	biimp3ar 1473	Infer implication from a logical equivalence. Similar to biimpar 477. (Contributed by NM, 2-Jan-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3anandis 1474	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3anandirs 1475	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ecase23d 1476	Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	3ecase 1477	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜃)    &   ⊢ (¬ 𝜓 → 𝜃)    &   ⊢ (¬ 𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	3bior1fd 1478	A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 937. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior1fand 1479	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 1480	A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 937. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3biant1d 1481	A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 531. (Contributed by Alexander van der Vekens, 26-Sep-2017.)
⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒 ∧ 𝜓)))
Theorem	intn3an1d 1482	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	intn3an2d 1483	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	intn3an3d 1484	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	an3andi 1485	Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)))
Theorem	an33rean 1486	Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) ↔ ((𝜑 ∧ 𝜏 ∧ 𝜌) ∧ ((𝜓 ∧ 𝜃) ∧ (𝜂 ∧ 𝜎) ∧ (𝜒 ∧ 𝜁))))
Theorem	3orel2 1487	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Eric Schmidt, 8-Oct-2025.)
⊢ (¬ 𝜓 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	3orel2OLD 1488	Obsolete version of 3orel2 1487 as of 8-Oct-2025. (Contributed by Scott Fenton, 26-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜓 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	3orel3 1489	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
⊢ (¬ 𝜒 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜓)))
Theorem	3orel13 1490	Elimination of two disjuncts in a triple disjunction. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜒) → ((𝜑 ∨ 𝜓 ∨ 𝜒) → 𝜓))
Theorem	3pm3.2ni 1491	Triple negated disjunction introduction. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ¬ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ ¬ 𝜒    ⇒   ⊢ ¬ (𝜑 ∨ 𝜓 ∨ 𝜒)
Theorem	an42ds 1492	Inference exchanging the last antecedent with the second one. See also an32s 653. (Contributed by Thierry Arnoux, 3-Jun-2025.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜒) ∧ 𝜓) → 𝜏)
1.2.12  Logical "nand" (Sheffer stroke)
Syntax	wnan 1493	Extend wff definition to include alternative denial ("nand").
wff (𝜑 ⊼ 𝜓)
Definition	df-nan 1494	Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1496 for an alternative. This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true ⊤ (df-tru 1545) and the constant false ⊥ (df-fal 1555), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1583), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1584), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1585), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1586). Contrast with ∧ (df-an 396), ∨ (df-or 849), → (wi 4), and ⊻ (df-xor 1514). (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
Theorem	nanan 1495	Conjunction in terms of alternative denial. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ⊼ 𝜓))
Theorem	dfnan2 1496	Alternative denial in terms of our primitive connectives (implication and negation). (Contributed by WL, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜑 → ¬ 𝜓))
Theorem	nanor 1497	Alternative denial in terms of disjunction and negation. This explains the name "alternative denial". (Contributed by BJ, 19-Oct-2022.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	nancom 1498	Alternative denial is commutative. Remark: alternative denial is not associative, see nanass 1512. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜓 ⊼ 𝜑))
Theorem	nannan 1499	Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	nanim 1500	Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜓)))