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