Definition df-nor 1520

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.)

Assertion

Ref	Expression
df-nor	⊢ ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

Detailed syntax breakdown of Definition 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 ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

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