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 1539) and the constant false ⊥ (df-fal 1549), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1585), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1587), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1589), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1590). Contrast with ∧ (df-an 399), ∨ (df-or 844), → (wi 4), ⊼ (df-nan 1481), and ⊻ (df-xor 1501). (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 1519 | . 2 wff (𝜑 ⊽ 𝜓) |
4 | 1, 2 | wo 843 | . . 3 wff (𝜑 ∨ 𝜓) |
5 | 4 | wn 3 | . 2 wff ¬ (𝜑 ∨ 𝜓) |
6 | 3, 5 | wb 208 | 1 wff ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
This definition is referenced by: norcom 1521 norcomOLD 1522 nornot 1523 nornotOLD 1524 noran 1525 noranOLD 1526 noror 1527 nororOLD 1528 norasslem1 1529 norass 1532 norassOLD 1533 trunortru 1585 trunortruOLD 1586 trunorfal 1587 trunorfalOLD 1588 falnorfal 1590 falnorfalOLD 1591 |
Copyright terms: Public domain | W3C validator |