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	syl3an1b 1401	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2b 1402	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3b 1403	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 ↔ 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an1br 1404	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2br 1405	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3br 1406	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜃 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syld3an3 1407	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)
Theorem	syld3an1 1408	A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)
Theorem	syld3an2 1409	A syllogism inference. (Contributed by NM, 20-May-2007.)
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3anl1 1410	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜓)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl2 1411	A syllogism inference. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂)
Theorem	syl3anl3 1412	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂)
Theorem	syl3anl 1413	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎)
Theorem	syl3anr1 1414	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr2 1415	A syllogism inference. (Contributed by NM, 1-Aug-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂)
Theorem	syl3anr3 1416	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂)
Theorem	3anidm12 1417	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm13 1418	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	3anidm23 1419	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	syl2an3an 1420	syl3an 1158 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜂)
Theorem	syl2an23an 1421	Deduction related to syl3an 1158 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜑) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜃 ∧ 𝜑) → 𝜂)
Theorem	3ori 1422	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)    ⇒   ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
Theorem	3jao 1423	Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
Theorem	3jaob 1424	Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.)
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)))
Theorem	3jaoi 1425	Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)
Theorem	3jaod 1426	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    &   ⊢ (𝜑 → (𝜏 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒))
Theorem	3jaoian 1427	Disjunction of three antecedents (inference). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜏 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	3jaodan 1428	Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒)
Theorem	mpjao3dan 1429	Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof shortened by Wolf Lammen, 20-Apr-2024.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mpjao3danOLD 1430	Obsolete version of mpjao3dan 1429 as of 17-Apr-2024. (Contributed by Thierry Arnoux, 13-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	3jaao 1431	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 1432	Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 → (𝜒 ↔ 𝜏))    &   ⊢ (𝜂 → (𝜏 ↔ 𝜁))    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁))
Theorem	3orbi123d 1433	Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	3anbi123d 1434	Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3anbi12d 1435	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂)))
Theorem	3anbi13d 1436	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))
Theorem	3anbi23d 1437	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi1d 1438	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	3anbi2d 1439	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))
Theorem	3anbi3d 1440	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒)))
Theorem	3anim123d 1441	Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁)))
Theorem	3orim123d 1442	Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜂 → 𝜁))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁)))
Theorem	an6 1443	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂)))
Theorem	3an6 1444	Analogue of an4 652 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ (𝜓 ∧ 𝜃 ∧ 𝜂)))
Theorem	3or6 1445	Analogue of or4 923 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃) ∨ (𝜏 ∨ 𝜂)) ↔ ((𝜑 ∨ 𝜒 ∨ 𝜏) ∨ (𝜓 ∨ 𝜃 ∨ 𝜂)))
Theorem	mp3an1 1446	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜑    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
Theorem	mp3an2 1447	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	mp3an3 1448	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mp3an12 1449	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	mp3an13 1450	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜑    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	mp3an23 1451	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3an1i 1452	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
⊢ 𝜓    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	mp3anl1 1453	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜑    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl2 1454	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜓    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	mp3anl3 1455	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
⊢ 𝜒    &   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
Theorem	mp3anr1 1456	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
⊢ 𝜓    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr2 1457	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
⊢ 𝜒    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜏)
Theorem	mp3anr3 1458	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
⊢ 𝜃    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)
Theorem	mp3an 1459	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	mpd3an3 1460	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	mpd3an23 1461	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	mp3and 1462	A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	mp3an12i 1463	mp3an 1459 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	mp3an2i 1464	mp3an 1459 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	mp3an3an 1465	mp3an 1459 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	mp3an2ani 1466	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	biimp3a 1467	Infer implication from a logical equivalence. Similar to biimpa 476. (Contributed by NM, 4-Sep-2005.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	biimp3ar 1468	Infer implication from a logical equivalence. Similar to biimpar 477. (Contributed by NM, 2-Jan-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3anandis 1469	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3anandirs 1470	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ecase23d 1471	Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	3ecase 1472	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
⊢ (¬ 𝜑 → 𝜃)    &   ⊢ (¬ 𝜓 → 𝜃)    &   ⊢ (¬ 𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	3bior1fd 1473	A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 933. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    ⇒   ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3bior1fand 1474	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 1475	A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 933. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
⊢ (𝜑 → ¬ 𝜃)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∨ 𝜒 ∨ 𝜓)))
Theorem	3biant1d 1476	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 1477	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	intn3an2d 1478	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	intn3an3d 1479	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	an3andi 1480	Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)))
Theorem	an33rean 1481	Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) ↔ ((𝜑 ∧ 𝜏 ∧ 𝜌) ∧ ((𝜓 ∧ 𝜃) ∧ (𝜂 ∧ 𝜎) ∧ (𝜒 ∧ 𝜁))))
Theorem	an33reanOLD 1482	Obsolete version of an33rean 1481 as of 21-Apr-2024. (Contributed by Thierry Arnoux, 14-Apr-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) ↔ ((𝜑 ∧ 𝜏 ∧ 𝜌) ∧ ((𝜓 ∧ 𝜃) ∧ (𝜂 ∧ 𝜎) ∧ (𝜒 ∧ 𝜁))))
1.2.12  Logical "nand" (Sheffer stroke)
Syntax	wnan 1483	Extend wff definition to include alternative denial ("nand").
wff (𝜑 ⊼ 𝜓)
Definition	df-nan 1484	Define incompatibility, or alternative denial ("not-and" or "nand"). See dfnan2 1486 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 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1580), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1581), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1582), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1583). Contrast with ∧ (df-an 396), ∨ (df-or 844), → (wi 4), and ⊻ (df-xor 1504). (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
Theorem	nanan 1485	Conjunction in terms of alternative denial. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ⊼ 𝜓))
Theorem	dfnan2 1486	Alternative denial in terms of our primitive connectives (implication and negation). (Contributed by WL, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜑 → ¬ 𝜓))
Theorem	nanor 1487	Alternative denial in terms of disjunction and negation. This explains the name "alternative denial". (Contributed by BJ, 19-Oct-2022.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	nancom 1488	Alternative denial is commutative. Remark: alternative denial is not associative, see nanass 1502. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜓 ⊼ 𝜑))
Theorem	nannan 1489	Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	nanim 1490	Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜓)))
Theorem	nannot 1491	Negation in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Revised by Wolf Lammen, 26-Jun-2020.)
⊢ (¬ 𝜑 ↔ (𝜑 ⊼ 𝜑))
Theorem	nanbi 1492	Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓))))
Theorem	nanbi1 1493	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒)))
Theorem	nanbi2 1494	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by Anthony Hart, 1-Sep-2011.) (Proof shortened by SF, 2-Jan-2018.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓)))
Theorem	nanbi12 1495	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃)))
Theorem	nanbi1i 1496	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒))
Theorem	nanbi2i 1497	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓))
Theorem	nanbi12i 1498	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃))
Theorem	nanbi1d 1499	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ⊼ 𝜃) ↔ (𝜒 ⊼ 𝜃)))
Theorem	nanbi2d 1500	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ⊼ 𝜓) ↔ (𝜃 ⊼ 𝜒)))