Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-nor | Structured version Visualization version GIF version |
Description: Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1546) and the constant false ⊥ (df-fal 1556), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1592), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1594), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1596), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1597). Contrast with ∧ (df-an 400), ∨ (df-or 848), → (wi 4), ⊼ (df-nan 1488), and ⊻ (df-xor 1508). (Contributed by Remi, 25-Oct-2023.) |
Ref | Expression |
---|---|
df-nor | ⊢ ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 1, 2 | wnor 1526 | . 2 wff (𝜑 ⊽ 𝜓) |
4 | 1, 2 | wo 847 | . . 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: norcom 1528 norcomOLD 1529 nornot 1530 nornotOLD 1531 noran 1532 noranOLD 1533 noror 1534 nororOLD 1535 norasslem1 1536 norass 1539 norassOLD 1540 trunortru 1592 trunortruOLD 1593 trunorfal 1594 trunorfalOLD 1595 falnorfal 1597 falnorfalOLD 1598 wl-df3maxtru1 35400 |
Copyright terms: Public domain | W3C validator |