Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-nan | Structured version Visualization version GIF version |
Description: 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 1531) and the constant false ⊥ (df-fal 1541), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1569), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1570), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1571), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1572). Contrast with ∧ (df-an 397), ∨ (df-or 842), → (wi 4), and ⊻ (df-xor 1496). (Contributed by Jeff Hoffman, 19-Nov-2007.) |
Ref | Expression |
---|---|
df-nan | ⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wnan 1475 | . 2 wff (𝜑 ⊼ 𝜓) |
4 | 1, 2 | wa 396 | . . 3 wff (𝜑 ∧ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ∧ 𝜓) |
6 | 3, 5 | wb 207 | 1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: nanan 1477 nanimn 1478 nanor 1479 nanbi 1484 xornan2 1504 trunanfal 1570 nic-mpALT 1664 nic-ax 1665 nic-axALT 1666 nfnan 1892 elnanel 9058 naim1 33634 naim2 33635 df3nandALT1 33644 imnand2 33647 waj-ax 33659 lukshef-ax2 33660 arg-ax 33661 nandsym1 33667 tsna1 35303 tsna2 35304 tsna3 35305 ifpdfnan 39730 ifpnannanb 39751 nanorxor 40514 undisjrab 40515 |
Copyright terms: Public domain | W3C validator |