Definition df-nor 1529

Description: Define joint denial ("not-or" or "nor"). After we define the constant true ⊤ (df-tru 1544) and the constant false ⊥ (df-fal 1554), we will be able to prove these truth table values: ((⊤ ⊽ ⊤) ↔ ⊥) (trunortru 1590), ((⊤ ⊽ ⊥) ↔ ⊥) (trunorfal 1591), ((⊥ ⊽ ⊤) ↔ ⊥) (falnortru 1592), and ((⊥ ⊽ ⊥) ↔ ⊤) (falnorfal 1593). Contrast with ∧ (df-an 397), ∨ (df-or 846), → (wi 4), ⊼ (df-nan 1490), and ⊻ (df-xor 1510). (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 1528	. 2 wff (𝜑 ⊽ 𝜓)
4	1, 2	wo 845	. . 3 wff (𝜑 ∨ 𝜓)
5	4	wn 3	. 2 wff ¬ (𝜑 ∨ 𝜓)
6	3, 5	wb 205	1 wff ((𝜑 ⊽ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))

This definition is referenced by:  norcom  1530  norcomOLD  1531  nornot  1532  noran  1533  noror  1534  norasslem1  1535  norass  1538  trunortru  1590  trunorfal  1591  falnorfal  1593  wl-df3maxtru1  36368