![]() |
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 1541) and the constant false ⊥ (df-fal 1551), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1579), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1580), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1581), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1582). Contrast with ∧ (df-an 400), ∨ (df-or 845), → (wi 4), and ⊻ (df-xor 1503). (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 1482 | . 2 wff (𝜑 ⊼ 𝜓) |
4 | 1, 2 | wa 399 | . . 3 wff (𝜑 ∧ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ∧ 𝜓) |
6 | 3, 5 | wb 209 | 1 wff ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: nanan 1484 nanimn 1485 nanor 1486 nanbi 1491 xornan2 1512 trunanfal 1580 nic-mpALT 1674 nic-ax 1675 nic-axALT 1676 nfnan 1901 elnanel 9054 naim1 33850 naim2 33851 df3nandALT1 33860 imnand2 33863 waj-ax 33875 lukshef-ax2 33876 arg-ax 33877 nandsym1 33883 tsna1 35582 tsna2 35583 tsna3 35584 ifpdfnan 40194 ifpnannanb 40215 nanorxor 41009 undisjrab 41010 |
Copyright terms: Public domain | W3C validator |